Generation/stack sul.

z3gi/sut/__init__.py

+from abc import ABCMeta, abstractmethod
+from typing import List
+
+import collections
+
+from model.ra import Action
+
+
+class SUT(metaclass=ABCMeta):
+    OK = "OK"
+    NOK = "NOK"
+    @abstractmethod
+    def run(self, seq:List[object]):
+        """Runs a sequence of inputs on the SUT and returns an observation"""
+        pass
+
+    @abstractmethod
+    def input_interface(self) -> List[object]:
+        """Runs the list of inputs or input signatures comprising the input interface"""
+        pass
+
+ActionSignature = collections.namedtuple("ActionSignature", ('label', 'num_params'))
+
+class ObjectSUT(SUT):
+    """Wraps a"""
+    def __init__(self, act_sigs, obj_gen):
+        self.obj_gen = obj_gen
+        self.acts = {act_sig.label:act_sig for act_sig in act_sigs}
+
+    def run(self, seq:List[object]):
+        obj = self.obj_gen()
+        values = set()
+        out_seq = []
+        for (label, val) in seq:
+            meth = obj.__getattribute__(label)
+            if self.acts[label].num_params == 0:
+                outp = meth()
+            else:
+                values.add(val)
+                outp = meth(val)
+            outp_action = self.parse_out(outp)
+            values.add(outp_action.value)
+            out_seq[:-1] = outp_action
+        return list(zip(seq, out_seq))
+
+
+    def parse_out(self, outp) -> Action:
+        fresh = None
+        if isinstance(outp, bool):
+            return Action(str(outp), fresh)
+        if isinstance(outp, str):
+            return Action(outp, fresh)
+        if isinstance(outp, int):
+            return  ("int", outp)
+        if isinstance(outp, tuple) and len(outp) == 2:
+            (lbl, val) = outp
+            if isinstance(val, int) and isinstance(lbl, str):
+                return outp
+        raise Exception("Cannot process output")
+
+    def input_interface(self) -> List[ActionSignature]:
+        return list(self.acts.values())
\ No newline at end of file

z3gi/sut/stack.py

+from sut import SUT, ObjectSUT, ActionSignature
+
+
+class Stack():
+    INTERFACE = [ActionSignature("get", 0), ActionSignature("put", 1)]
+    def __init__(self, size):
+        super()
+        self.size = size
+        self.list = list()
+
+    def get(self):
+        if len(self.list) == 0:
+            return SUT.OK
+        else:
+            return ("OGET", self.list.pop())
+
+    def put(self, val):
+        if len(self.list) < self.size:
+            self.list.append(val)
+            return SUT.OK
+        else:
+            return SUT.NOK
+
+
+def new_stack_sul(size):
+    return ObjectSUT(lambda : Stack(size), Stack.INTERFACE)

z3gi/test/__init__.py

+import itertools
 from abc import ABCMeta, abstractmethod
-
-import collections
 from typing import List
 
-import itertools
-
 from model import Automaton, Acceptor
 from model.fa import MealyMachine
 from model.ra import IORegisterAutomaton, Action

z3gi/test/generation.py

+from abc import ABCMeta, abstractmethod
+from typing import List
+from sut import SUT, ActionSignature
+
+
+# class RAObservation():
+#     def __init__(self, trace):
+#         self.trace = trace
+#
+#     def values(self):
+#         for
+
+class ObservationGeneration(metaclass=ABCMeta):
+
+    @abstractmethod
+    def generate_observations(self, max_depth) -> List[object]:
+        pass
+
+class ExhaustiveRAGenerator(ObservationGeneration):
+    def __init__(self, sut:SUT, act_sigs:List[ActionSignature]):
+        self.sut = sut
+        self.act_sigs = act_sigs
+        for sig in act_sigs:
+            if sig.num_params > 1:
+                raise Exception("This generator assumes at most one parameter per action")
+
+    def generate_observations(self, max_depth, max_registers=3) -> List[list]:
+        return self._generate_observations([0,[]], 0, max_depth, max_registers)
+
+    def _generate_observations(self, prev_obs, crt_depth, max_depth, max_values):
+        if crt_depth > max_depth:
+            return []
+        else:
+            new_obs = []
+            for (num_val, obs) in prev_obs:
+                for act_sig in self.act_sigs:
+                    label = act_sig.label
+                    if act_sig.num_params == 1:
+                        for i in range(0, max(num_val, max_values)):
+                            seq = [inp for (inp, _) in obs]
+                            seq.append((label, i))
+                            new_obs[:-1] = (max(num_val, i), self.sut.run(seq))
+                    else:
+                        seq = [inp for (inp, _) in obs]
+                        seq = seq.append((label, None))
+                        new_obs[:-1] = (num_val, self.sut.run(seq))
+
+            if crt_depth < max_depth:
+                new_obs.extend(self._generate_observations(new_obs, crt_depth+1, max_depth, max_values))
+            return  new_obs
+