module Automaton[StateSpace, Labels, NoInput] -- Usual definition of an automaton -- (deterministic as well as nondeterministic). -- copyright Richard St-Denis, Universite de Sherbrooke, 2015. -- Labels can be an alphabet, an event set or a set of -- input/output (mealy machine). -- NoInput is the no input symbol (usually epsilon or lambda). open util/ternary as UTIL abstract sig Automaton { states : set StateSpace, labels : set Labels, transition : set StateSpace->(Labels+NoInput)->StateSpace, initialState : one StateSpace, finalStates : set StateSpace } { transition.dom + transition.ran in states transition.mid in labels+NoInput initialState in states finalStates in states } fun dualTransition[A: one Automaton] : (Labels+NoInput)->StateSpace->StateSpace { UTIL/flip12[A.transition] } -- Nondeterminism fun nonDeterministicTransitions[A: one Automaton] : StateSpace->Labels { { s1: StateSpace, lbl : Labels | some s2, s3 : StateSpace | s1->lbl->s2 in A.transition and s1->lbl->s3 in A.transition and not s2 = s3 } } fun epsTransitions[A: one Automaton] : StateSpace { (A.transition.StateSpace).NoInput } pred isDeterministic[A: one Automaton] { no nonDeterministicTransitions[A] and no epsTransitions[A] } -- Reachability and coreachability fun getTransition[A: one Automaton, L: set Labels+NoInput] : StateSpace->StateSpace { -- Return the unlabelled (binary) transition relation of A -- w.r.t. the label set L. L.(dualTransition[A]) } fun target[A: one Automaton, s: one StateSpace, lbl: one Labels+NoInput] : set StateSpace { (getTransition[A,lbl])[s] } fun getReachableStates[A: one Automaton, S: set StateSpace, L: set Labels+NoInput] : 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 Labels+NoInput] : set StateSpace { -- Return the coreachable states to the set of states S S.*(~(getTransition[A, L])) } pred trim[A1, A2: one Automaton, L: set Labels+NoInput] { A1.labels = A2.labels A1.initialState = A2.initialState let S = getReachableStates[A2, A2.initialState, L] & getCoreachableStates[A2, A2.finalStates, L] | A1.states = S and A1.finalStates = A2.finalStates & S and A1.transition = A2.transition & (S->L->S) } pred isTrim[A: one Automaton] { A.trim[A, A.labels+NoInput] } -- Restriction and subautomaton pred isARestriction[A1, A2: one Automaton, S: set StateSpace] { A1.states = A2.states & S and A1.labels = A2.labels and A1.transition = A1.states <: A2.transition :> A1.states and A1.initialState = A2.initialState & A1.states and A1.finalStates = A2.finalStates & A1.states } fun restriction[A: one Automaton, S: set StateSpace] : one Automaton { { X : Automaton | X.isARestriction[A, S] } } pred isSubautomaton[A1, A2: one Automaton] { A1.states in A2.states and A1.labels = A2.labels and A1.transition = A1.states <: A2.transition :> A1.states and A1.initialState = A2.initialState & A1.states and A1.finalStates = A2.finalStates & A1.states } ----------------------------------------------------- -- Silent events for the observer property sig SilentEvents in Labels { } pred isSilent[lbl: one Labels] { lbl in SilentEvents } abstract sig Walk { -- A walk with a single vertex is accepted. edges : seq Labels+NoInput, -- a sequence of edges vertices : seq StateSpace, -- a sequence of vertices stg : one Automaton -- in a state transition graph } { all k : Int | -- The first vertex is the initial state of the transition graph. vertices[0] = stg.initialState -- The number of vertices is one more than the number of edges. and #edges = minus[#vertices, 1] -- vertices[k-1] edges[k-1] vertices[k] => a transition s1->lbl->s2. and ((k >= 1 and k <= lastIdx[vertices]) implies let lbl = edges[minus[k, 1]] | let s1 = vertices[minus[k, 1]] | let s2 = vertices[k] | lbl.isSilent implies s2 = s1 else s2 in stg.target[s1, lbl]) } fact { -- Different walks have different vertices or different edges -- This fact can cause a problem with concatenation of a walk -- with an empty walk. all w1, w2 : Walk | not w1 = w2 implies ( (not w1.vertices = w2.vertices) or (not w1.edges = w2.edges)) } fun walkLength[w: one Walk] : Int { #inds[w.edges] } fun walkSize[w: one Walk] : Int { #inds[w.vertices] } fun lastLabel[w : one Walk] : one Labels { last[w.edges] } fun lastVertex[w: one Walk] : one StateSpace { last[w.vertices] } fun extension[w: one Walk, lbl: one Labels+NoInput] : one Walk { { x : Walk | x.stg = w.stg and x.edges = w.edges.insert[#w.edges, lbl] } } fun projectWalk[w: one Walk, L: set Labels] : set Int->Labels { { j : Int, lbl : Labels | (some k : w.edges.inds | w.edges[k] in L and lbl = w.edges[k] and #(w.edges.subseq[0,k].indsOf[L]) = plus[j,1]) } } pred isAnExtension[w: one Walk, lbl: one Labels+NoInput] { some s : StateSpace | w.lastVertex->lbl->s in w.stg.transition } pred isEmpty[w: one Walk] { walkLength[w] = 0 } pred isASingleton[w: one Walk, lbl: one Labels+NoInput] { w.edges.first = lbl and walkLength[w] = 1 } pred IsSilentUntil[w: one Walk, L: set Labels+NoInput] { lastLabel[w] in L and isSilent[elems[w.edges.butlast]] } pred isAccepted[w: one Walk] { -- the last vertex of the walk is a final state some (lastVertex[w] & w.stg.finalStates) } pred isAcceptedBy[w: one Walk, A: one Automaton] { A = w.stg and w.isAccepted } pred accept[A: one Automaton, w: one Walk] { w.isAcceptedBy[A] } ----------------------------------------------------- abstract sig Trace { symbols : seq Labels -- a sequence of labels } fact { -- different traces have different symbols all t1, t2 : Trace | not t1 = t2 implies not t1.symbols = t2.symbols } fun walkToTrace[w: one Walk, L: set Labels] : one Trace { { t : Trace | (all k : w.edges.inds | some j : Int | w.edges[k] in L implies t.symbols[j] = w.edges[k] and #(w.edges.subseq[0,k].indsOf[L]) = plus[j,1]) and #t.symbols = minus[#w.edges,#w.edges.indsOf[(Labels+NoInput)-L]] } }