Added more sut related classes. Now we should be able to create SUTs for all formalisms.

z3gi/sut/__init__.py

 from abc import ABCMeta, abstractmethod
-from typing import List, Tuple
+from typing import List, Tuple, Dict
 
 import collections
 
@@ -111,15 +111,31 @@ class SUTType(Enum):
 
 
 class SUTClass(metaclass=ABCMeta):
-    def __init__(self, sut_dict):
-        self.sut_dict = sut_dict
+    """for a class of systems (say stacks, or logins) provides means of instantiating SUTs of different types"""
 
-    def get_sut(self, sut_type : SUTType) -> SUT:
-        return self.sut_dict[sut_type]
-
-    def has_sut(self, sut_type : SUTType) -> bool:
-        return  sut_type in self.sut_dict
+    @abstractmethod
+    def new_sut(self, sut_type : SUTType) -> SUT:
+        """ builds a new SUT of the specified type. Returns None is no such SUT can be generated"""
+        pass
 
+class ScalableSUTClass(SUTClass, metaclass=ABCMeta):
+    """provides instantiation for scalable SUTs. Scalable SUTs are classes whose constructor take a size >0 integer
+    as an argument. This class also adds wrappers corresponding to the type (all SUTs are assumed to be ObjectSULs)."""
+
+    def __init__(self, sut_type_dict:Dict[SUTType,type]):
+        self.sut_type_dict = sut_type_dict
+
+    def new_sut(self, sut_type : SUTType, size :int):
+        if sut_type in self.sut_type_dict:
+            sut_obj = self.sut_type_dict[sut_type](size)
+            sut = sut_obj if sut_type is SUTType.IORA else \
+                RAWrapper(sut_obj) if sut_type is SUTType.RA else \
+                MealyWrapper(sut_obj) if sut_type is SUTType.Mealy else \
+                DFAWrapper(MealyWrapper(sut_obj)) if sut_type is SUTType.DFA else \
+                    None # no support for Moore Machines (yet)
+            return sut
+        else:
+            return None
 
 ActionSignature = collections.namedtuple("ActionSignature", ('label', 'num_params'))
 class RASUT(metaclass=ABCMeta):
@@ -200,11 +216,11 @@ class RAWrapper(RASUT):
         self.sut = sut
 
     def run(self, seq: List[Action]):
-        iora_obs = self.sut.run(seq)
-        seq = iora_obs.inputs()
         if len(seq) == 0:
             return RAObservation(seq, True)
         else:
+            iora_obs = self.sut.run(seq)
+            seq = iora_obs.inputs()
             trace = iora_obs.trace()
             (_, out) = trace[-1]
             acc = out.label is SUT.OK

z3gi/sut/fifoset.py

-from sut import SUT, ObjectSUT, ActionSignature
+from sut import SUT, ObjectSUT, ActionSignature, ScalableSUTClass, SUTType
 
 
 class FIFOSet():
@@ -12,7 +12,7 @@ class FIFOSet():
         if len(self.list) == 0:
             return SUT.NOK
         else:
-            return ("OGET", self.list.pop(len(self.list)-1))
+            return ("OGET", self.list.pop())
 
     def put(self, val):
         if len(self.list) < self.size and val not in self.list:
@@ -21,6 +21,60 @@ class FIFOSet():
         else:
             return SUT.NOK
 
+class RAFIFOSet():
+    INTERFACE = [ActionSignature("get", 1), ActionSignature("put", 1)]
+
+    def __init__(self, size):
+        super()
+        self.size = size
+        self.list = list()
+
+    def get(self, val):
+        if len(self.list) == 0:
+            return SUT.NOK
+        else:
+            if self.list[-1] == val:
+                self.list.pop()
+                return SUT.OK
+            else:
+                return SUT.NOK
+
+    def put(self, val):
+        if len(self.list) < self.size and val not in self.list:
+            self.list.append(val)
+            return SUT.OK
+        else:
+            return SUT.NOK
+
+class MealyFIFOSet():
+    INTERFACE = [ActionSignature("get", 0), ActionSignature("put", 0)]
+    def __init__(self, size):
+        super()
+        self.size = size
+        self.stored = 0
+
+    def get(self):
+        if self.stored == 0:
+            return SUT.NOK
+        else:
+            self.stored -= 1
+            return SUT.OK
+
+    def put(self, val):
+        if self.stored == self.size:
+            return SUT.NOK
+        else:
+            self.stored += 1
+            return SUT.OK
+
+class FIFOSetClass(ScalableSUTClass):
+    def __init__(self):
+        super({
+            SUTType.IORA: FIFOSet,
+            SUTType.RA: RAFIFOSet,
+            SUTType.Mealy: MealyFIFOSet,
+            SUTType.DFA: MealyFIFOSet
+        })
 
 def new_fifoset_sut(size):
     return ObjectSUT(FIFOSet.INTERFACE, lambda : FIFOSet(size))

z3gi/sut/stack.py

@@ -21,6 +21,30 @@ class Stack():
         else:
             return SUT.NOK
 
+class RAStack():
+    INTERFACE = [ActionSignature("get", 1), ActionSignature("put", 1)]
+
+    def __init__(self, size):
+        super()
+        self.size = size
+        self.list = list()
+
+    def get(self, val):
+        if len(self.list) == 0:
+            return SUT.NOK
+        else:
+            if val == self.list[-1]:
+                self.list.pop()
+                return SUT.OK
+            else:
+                return SUT.NOK
+
+    def put(self, val):
+        if len(self.list) < self.size:
+            self.list.append(val)
+            return SUT.OK
+        else:
+            return SUT.NOK
 
 def new_stack_sut(size):
     return ObjectSUT(Stack.INTERFACE, lambda : Stack(size))