Added untested RA model plus export function. Modified export function.

z3gi/define/__init__.py

@@ -2,6 +2,6 @@ from abc import ABCMeta, abstractmethod
 
 class Automaton(metaclass=ABCMeta):
     @abstractmethod
-    def export(self):
+    def export(self, model):
         """Returns a z3gi.model for this automaton."""
         pass
\ No newline at end of file

z3gi/define/ra.py

 from collections import namedtuple
 
 import z3
+from z3gi.model.ra import *
+from abc import ABCMeta, abstractmethod
+
 
 from z3gi.define import Automaton
 
@@ -19,8 +22,10 @@ class RegisterAutomaton(Automaton):
         self.guard = z3.Function('guard', self.Location, self.Label, self.Register)
         self.update = z3.Function('update', self.Location, self.Label, self.Register)
 
-    def export(self):
-        pass
+    def export(self, model):
+        builder = RegisterAutomatonBuilder(self)
+        ra = builder.build_ra(model, self.locations, self.labels, self.registers)
+        return ra
 
 
 def enum(name, elements):
@@ -29,3 +34,90 @@ def enum(name, elements):
         d.declare(element)
     d = d.create()
     return d, [d.__getattribute__(element) for element in elements]
+
+
+class RegisterAutomatonBuilder():
+    """
+    Builder class that construct a register automaton out of a model definition.
+    """
+    def __init__(self, ra):
+        super().__init__()
+        self.ra = ra
+
+
+    def build_ra(self, model, states, labels, regs):
+        mut_ra = MutableRegisterAutomaton()
+        translator = Translator(self.ra)
+        self._add_states(model, translator, mut_ra, states, labels, regs)
+        self._add_transitions(model, translator, mut_ra, states, labels, regs)
+        return mut_ra.to_immutable()
+
+    def _add_states(self, model, translator, mut_ra, z3states):
+        for z3state in z3states:
+            z3acc = model.eval(model.eval(self.ra.output(z3state)))
+            mut_ra.add_state(translator.z3_to_state(z3state), translator.z3_to_acc(z3acc) )
+
+    def _add_transitions(self, model, translator, mut_ra, z3state, z3label, z3regs):
+        registers_used = []
+        next_trans = []
+        z3end_state_to_guards = dict()
+        enabled_z3guards = [guard for guard in z3regs if
+                          model.eval(self.ra.guard(z3state, z3label, guard))]
+        for z3guard in enabled_z3guards:
+            z3end_state = model.eval(self.ra.transition(z3state, z3label, z3guard))
+            if z3end_state not in z3end_state_to_guards:
+                z3end_state_to_guards[z3end_state] = []
+            z3end_state_to_guards[z3end_state].append(z3guard)
+
+        update = model.eval(self.ra.update(z3state, z3label))
+        start_state = translator.z3_to_state(z3state)
+
+        for (z3end_state, z3guards) in z3end_state_to_guards.items():
+            guard = translator.z3_to_guard(z3guards)
+            z3asg = update if self.ra.fresh in z3guards else None
+            asg = translator.z3_to_assignment(z3asg)
+            end_state = translator.z3_to_state(z3end_state)
+            transition = RATransition(start_state, translator.z3_to_label(z3label),
+                                      guard, asg, end_state)
+            mut_ra.add_transition(start_state, transition)
+
+
+class Translator():
+    """Provides translation from z3 constants to RA elements. """
+    def __init__(self, ra):
+        super.__init__()
+        self.reg_context = dict()
+        self.ra = ra
+
+    def z3_to_assignment(self, z3asg):
+        if z3asg is None:
+            asg = NoAssignment()
+        else:
+            asg = RegisterAssignment(self.z3_to_register(z3asg))
+        return asg
+
+    def z3_to_guard(self, z3guards):
+        guard_regs = [self.z3_to_register(z3reg) for z3reg in z3guards if z3reg is not self.ra.fresh]
+        if self.ra.fresh in z3guards:
+            return FreshGuard(guard_regs)
+        else:
+            equ_guards = [EqualityGuard(guard_reg) for guard_reg in guard_regs]
+            if len(equ_guards) == 1:
+                return equ_guards[0]
+            else:
+                return OrGuard(equ_guards)
+
+    def z3_to_acc(self, z3acc):
+        return str(z3acc) == "True"
+
+    def z3_to_state(self, z3state):
+        return str(z3state)
+
+    def z3_to_label(self, z3label):
+        return str(z3label)
+
+    def z3_to_register(self, z3register):
+        assert z3register is not self.ra.fresh
+        if self.reg_context[z3register] is None:
+            self.reg_context = Register(self.ra.registers.index(z3register))
+        return self.reg_context[z3register]
\ No newline at end of file

z3gi/model/__init__.py

@@ -4,20 +4,20 @@ from abc import ABCMeta, abstractmethod
 class Automaton(metaclass=ABCMeta):
    def __init__(self, states, state_to_trans):
       super().__init__()
-      self.states = states
-      self.state_to_trans = state_to_trans
+      self._states = states
+      self._state_to_trans = state_to_trans
 
    def start_state(self):
-      return self.states[0]
+      return self._states[0]
 
    def states(self):
-      return list(self.states)
+      return list(self._states)
 
    def transitions(self, state, label=None):
       if label is None:
-         return list(self.state_to_trans[state])
+         return list(self._state_to_trans[state])
       else:
-         return list([trans for trans in self.state_to_trans[state] if trans.start_label == label])
+         return list([trans for trans in self._state_to_trans[state] if trans.start_label == label])
 
    @abstractmethod
    def state(self, trace):
@@ -36,10 +36,10 @@ class Transducer(Automaton, metaclass=ABCMeta):
 class Acceptor(Automaton, metaclass=ABCMeta):
     def __init__(self, states, state_to_trans, state_to_acc):
         super.__init__(states, state_to_trans)
-        self.state_to_acc = state_to_acc
+        self._state_to_acc = state_to_acc
 
     def is_accepting(self, state):
-        return self.state_to_acc[state]
+        return self._state_to_acc[state]
 
     def accepts(self, trace):
         state = self.state(trace)
@@ -54,10 +54,10 @@ class Transition():
         self.end_state = self.end_state
 
 
-"""Exception raised when no transition could be fired"""
+"""Exception raised when no transition can be fired"""
 class NoTransitionFired(Exception):
    pass
 
-"""Exception raised when several transitions could be fired in a deterministic machine"""
-class NonDeterminism(Exception):
+"""Exception raised when several transitions can be fired in a deterministic machine"""
+class MultipleTransitionsFired(Exception):
     pass
\ No newline at end of file

z3gi/model/ra.py

-from z3gi.model import Transition, Acceptor, NoTransitionFired, NonDeterminism
+from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired
 from abc import ABCMeta, abstractmethod
+import itertools
 
 class RegisterAutomaton(Acceptor):
     def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
       super.__init__(locations, loc_to_trans, loc_to_acc)
-      self.register = registers
+      self._registers = registers
+
+    def get_registers(self):
+        return self._registers
 
     def state(self, trace):
         init = -1
         reg_val = dict()
-        for reg in self.ra.get_registers():
+        for reg in self.get_registers():
             reg_val[reg] = init
 
         crt_state = self.start_state()
@@ -22,20 +26,45 @@ class RegisterAutomaton(Acceptor):
             if len(fired_transitions) == 0:
                 raise NoTransitionFired
 
+            if len(fired_transitions) > 1:
+                raise MultipleTransitionsFired
+
             fired_transition = fired_transitions[0]
             reg_val = fired_transition.update(reg_val, action)
             crt_state = fired_transition.end_state
 
         return crt_state
 
+class MutableRegisterAutomaton(RegisterAutomaton):
+    def __init__(self):
+        super.__init__([], dict(), dict())
+
+    def add_state(self, state, accepts):
+        if state not in self._states:
+            self._states.append(state)
+        self._state_to_acc[state] = accepts
+
+
+    def add_transition(self, state, transition):
+        if state not in self._state_to_trans:
+            self._state_to_trans[state]=[]
+        self._state_to_trans[state].append(transition)
+        for reg in transition.guard.get_registers():
+            if reg not in self._registers:
+                self._registers.append(reg)
+
+    def to_immutable(self):
+        return RegisterAutomaton(self._states, self._state_to_acc, self._state_to_trans, self._registers)
+
+
 class RATransition(Transition):
     def __init__(self, start_state, start_label, guard, assignment, end_state):
-        Transition.__init__(start_state, start_label, end_state)
+        super.__init__(start_state, start_label, end_state)
         self.guard = guard
         self.assignment = assignment
 
     def is_enabled(self, action, valuation):
-        if action.label == self.start_label:
+        if action.label is self.start_label:
             satisfied = self.guard.is_satisfied(action.value, valuation)
             return satisfied
         return False
@@ -43,17 +72,22 @@ class RATransition(Transition):
     def update(self, action, valuation):
         return self.assignment.update(valuation, action.value)
 
-
+"""A guard with is_satisfied implements a predicate over the current register valuation and the parameter value. """
 class Guard(metaclass=ABCMeta):
     def __init__(self):
         pass
 
+    """Returns the registers/constants over which the guard is formed"""
+    @abstractmethod
+    def get_registers(self):
+        pass
+
     # to make this more abstract, value would have to be replaced by param valuation
     @abstractmethod
     def is_satisfied(self, valuation, value):
         pass
 
-
+"""An equality guard holds iff. the parameter value is equal to the value assigned to its register."""
 class EqualityGuard(Guard):
     def __init__(self, register):
         super.__init__()
@@ -62,6 +96,9 @@ class EqualityGuard(Guard):
     def is_satisfied(self, valuation, value):
         return valuation[self.register] == value
 
+    def get_registers(self):
+        return [self.register]
+
 
 class OrGuard(Guard):
     def __init__(self, guards):
@@ -73,7 +110,15 @@ class OrGuard(Guard):
                 return True
         return False
 
+    def get_registers(self):
+        regs_of_guards = [guard.get_registers() for guard in self.guards]
+        regs = itertools.chain.from_iterable(regs_of_guards)
+        seen = set()
+        distinct_regs = [x for x in regs if x not in seen and not seen.add(x)]
+        return list(distinct_regs)
+
 
+"""An fresh guard holds if the parameter value is different from the value assigned to any of its registers."""
 class FreshGuard(Guard):
     def __init__(self, guarded_registers = []):
         super.__init__()
@@ -85,7 +130,10 @@ class FreshGuard(Guard):
                 return False
         return True
 
+    def get_registers(self):
+        return self.registers
 
+"""An assignment updates the valuation of registers using the old valuation and the current parameter value"""
 class Assignment(metaclass=ABCMeta):
     def __init__(self):
         pass
@@ -102,10 +150,26 @@ class RegisterAssignment(Assignment):
         self.register = register
 
     def update(self, valuation, value):
-        valuation[self.register] = value
+        new_valuation = dict(valuation)
+        new_valuation[self.register] = value
+        return new_valuation
 
 class NoAssignment(Assignment):
     def __init__(self):
         super.__init__()
     def update(self, valuation):
-        return valuation
\ No newline at end of file
+        return dict(valuation)
+
+"""Symbolic values can be used to symbolically express registers, constants and parameters."""
+class SymbolicValue(metaclass=ABCMeta):
+    def __init__(self, index):
+        super.__init__()
+        self.index = index
+
+
+class Register(SymbolicValue):
+    def __init__(self, index):
+        super.__init__(index)
+
+    def __str__(self):
+        return "r" + str(self.index)