Automaton Alloy

/*
* Modeling the strututure and execution of deterministic finite automata.
* FEUP, MFES, 22 Nov 2016
*/
open util/ordering[ExecutionState]

sig State {}

sig Symbol{}

sig Automaton {
	states:  set State,
	alphabet: set Symbol,
	transitions: (states -> alphabet) -> one states,
	start: states,
	accepting: set states
}{
	-- all states are reachable from start
	states = start.* {s, s': states | some s.transitions.s'}
}

sig ExecutionState {
	automaton: Automaton,
	current: State,
	lastSymbol: lone Symbol
} {
	current in automaton.states
	lastSymbol in automaton.alphabet
}

pred start[a: Automaton, e': ExecutionState] {
	e'.automaton = a
	e'.current = a.start
	no e'.lastSymbol
}

pred input[e: ExecutionState, s: Symbol, e': ExecutionState] {
	s in e.automaton.alphabet
	e'.automaton = e.automaton
	e'.current = e.automaton.transitions[e.current][s]
	e'.lastSymbol = s
}

fact validTraces {
	some a: Automaton | start[a, first]
	all e: ExecutionState, e': e.next | some s: Symbol | input[e, s, e']
}

one sig N1, N2, N3, N0 extends State{}

one sig A, B, C extends Symbol{}

pred Automata [a: Automaton] {
	a.states = N1 + N2 + N3 + N0
	a.alphabet = A + B + C
	a.transitions = ((N1->A)->N2) + ((N1->B)->N2) + ((N1->C)->N0) + ((N2->A)->N1) + ((N2->B)->N2) + ((N2->C)->N3) +
					((N3->A)->N0) + ((N3->B)->N0) + ((N3->C)->N2) + ((N0->A)->N0) + ((N0->B)->N0) + ((N0->C)->N0)
	a.start = N1
	a.accepting = N3
}

run findTraceAccepting {
	Automata[first.automaton]
	last.current in last.automaton.accepting
} for 7 but exactly 1 Automaton