module Automaton[StateSpace, Label, SeqIdx] -- Usual definition of an automaton. -- copyright Richard St-Denis, Universite de Sherbrooke, 2013. open util/ternary as UTIL open util/ordering[SeqIdx] as ORD abstract sig Automaton { states : set StateSpace, labels : set Label, transition : set StateSpace -> Label -> StateSpace, initialState : one StateSpace, finalStates : set StateSpace } { transition.dom + transition.ran in states transition.mid in labels initialState in states finalStates in states } -- Events for spontaneous transitions sig SilentEvents in Label { } pred IsSilent [l: one Label] { l in SilentEvents } -- Automaton augmented with controllable events abstract sig CtrlAutomaton extends Automaton { events : set Label, controllableEvents : set Label, markedStates : set StateSpace } { events = labels controllableEvents in labels markedStates = finalStates } fun dualTransition[A: one Automaton] : Label -> StateSpace -> StateSpace { UTIL/flip12[A.transition] } fun GetTransition[A: one Automaton, L: set Label] : StateSpace -> StateSpace { -- return the unlabelled (binary) transition relation of G -- w.r.t. the label set L L.(dualTransition[A]) } fun target[A: one Automaton, s: one StateSpace, l: one Label] : one StateSpace { (GetTransition[A,l])[s] } fun GetReachableStates[A: one Automaton, S: set StateSpace, L: set Label] : set StateSpace { -- return the reachable states from the set of states S S.*(GetTransition[A, L]) } fun GetCoreachableStates[A: one Automaton, S: set StateSpace, L: set Label] : set StateSpace { -- return the coreachable states to the set of states S S.*(~(GetTransition[A, L])) } pred Trim[A1, A2: one Automaton, L: set Label] { A1.initialState = A2.initialState let S = GetReachableStates[A2, A2.initialState, L] & GetCoreachableStates[A2, A2.finalStates, L] | A1.transition = A2.transition & (S->L->S) and A1.finalStates = A2.finalStates & S } pred IsTrim[A: one Automaton] { A.Trim[A, Label] } pred IsARestriction[B, A: one Automaton, S: set StateSpace] { B.states = A.states & S and B.labels = A.labels and B.transition = B.states <: A.transition :> B.states and B.initialState = A.initialState & B.states and B.finalStates = A.finalStates & B.states } fun Restriction[A: one Automaton, S: set StateSpace] : one Automaton { { B : Automaton | B.IsARestriction[A, S] } } pred IsReduced[B, A: one Automaton] { B.states in A.states and B.labels = A.labels and B.transition = B.states <: A.transition :> B.states and B.initialState = A.initialState & B.states and B.finalStates = A.finalStates & B.states } ----------------------------------------------------- sig Walk { edges : SeqIdx -> lone Label, -- a sequence of edges vertices : SeqIdx -> lone StateSpace, -- a sequence of vertices graph : one Automaton -- in a transition graph } { -- Label and StateSpace cover only an initial segment of SeqIdx (all k : SeqIdx - ORD/first[] | some k.edges implies some ORD/prev[k].edges) and (all k : SeqIdx - ORD/first[] | some k.vertices implies some ORD/prev[k].vertices) and -- the first vertex is the initial state of the transition graph (ORD/first[].vertices = graph.initialState) and -- the number of vertices is one more than the number of edges (ORD/max[edges.Label].ORD/next[] = ORD/max[vertices.StateSpace]) and (all k : SeqIdx | -- vertices[k] edges[k] vertices[k+1] => a transition s->l->s' (ORD/lte[k, ORD/max[edges.Label]] implies let l = k.edges | let s = k.vertices | let s' = (k.ORD/next[]).vertices | IsSilent[l] implies s' = s else s' = graph.target[s, l])) } fact { -- different walks have different edges (no two sequences are identical) no w, w' : Walk | not w = w' && w.edges = w'.edges } fun walkLength[w: one Walk] : Int { #w.edges } fun walkSize[w: one Walk] : Int { #w.vertices } fun lastLabel[w : one Walk] : one Label { ORD/max[(w.edges).Label].(w.edges) } fun lastVertex[w: one Walk] : one StateSpace { ORD/max[(w.vertices).StateSpace].(w.vertices) } fun Extension[w: one Walk, l: one Label] : one Walk { { w' : Walk | let lastIdxEdges = ORD/max[(w'.edges).Label] | w'.graph = w.graph and lastIdxEdges = ORD/max[(w.vertices).StateSpace] and (all k : (w.edges).Label | k.(w'.edges) = k.(w.edges)) and lastIdxEdges.(w'.edges) = l } } fun Concatenation[w1: one Walk, w2: one Walk] : one Walk { { w : Walk | w.graph = w1.graph and w.graph = w2.graph and (all k : (w1.edges).Label | k.(w.edges) = k.(w1.edges)) and (all k : (w2.edges).Label | some j : SeqIdx { ORD/gt[j, ORD/max[(w1.edges).Label]] and j.(w.edges) = k.(w2.edges) and j.(w.vertices) = k.(w2.vertices) and #ORD/prevs[k] = #(ORD/prevs[j] -ORD/prevs[ORD/max[(w1.vertices).StateSpace]]) } ) and ORD/max[(w.vertices).StateSpace].(w.vertices) = ORD/max[(w2.vertices).StateSpace].(w2.vertices) } } pred IsASingleton[w: one Walk, l: one Label] { ORD/first[].(w.edges) = l -- the walk length is one and ORD/first[] = ORD/max[(w.edges).Label] -- and walkLength[w] = 1 -- to avoid Int } pred IsSilentUntil[w: one Walk, L: set Label] { let lastIdxEdges = ORD/max[(w.edges).Label] | -- the last label belongs to L lastIdxEdges.(w.edges) in L -- all other labels are silent and (all k : SeqIdx | ORD/lt[k, lastIdxEdges] implies k.(w.edges) in SilentEvents) } pred IsAccepted[w: one Walk] { -- the last vertex of the walk is a final state in the transition graph ORD/max[(w.vertices).StateSpace].(w.vertices) in w.graph.finalStates } pred IsAcceptedBy[w: one Walk, A: one Automaton] { A = w.graph w.IsAccepted } pred Accept[A: one Automaton, w: one Walk] { w.IsAcceptedBy[A] } pred LastStepIsCtrl[w: one Walk] { ORD/max[(w.edges).Label].(w.edges) in w.graph.controllableEvents }