Commit 482b2fa2 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Added DFA model.

parent 56e6339e
......@@ -158,7 +158,7 @@ class RAEncoder(Encoder):
)
),
# If a non-fresh register is updated, and c and n are connect by fresh,
# If a non-fresh register is updated, and c and n are connected by fresh,
# then in c there is a register whose value is v,
# else the valuation is maintained.
z3.ForAll(
......
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired
from abc import ABCMeta, abstractmethod
import itertools
import collections
from typing import List
Symbol = str
State = str
Label = str
class DFA(Acceptor):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
super().__init__(locations, loc_to_trans, loc_to_acc)
self._registers = registers
def transitions(self, state: State, label:Label = None) -> List[Transition]:
return super().transitions(state, label)
def state(self, trace: List[Symbol]) -> State:
crt_state = self.start_state()
tr_str = crt_state
for symbol in trace:
transitions = self.transitions(crt_state, symbol)
fired_transitions = [trans for trans in transitions if trans.start_label == symbol]
# the number of fired transitions can be more than one since we could have multiple equalities
if len(fired_transitions) == 0:
raise NoTransitionFired
if len(fired_transitions) > 1:
raise MultipleTransitionsFired
fired_transition = fired_transitions[0]
crt_state = fired_transition.end_state
tr_str += " {0} {1}".format(symbol, crt_state)
# print(tr_str)
return crt_state
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment