Getting stuck on the basics

Questions
1

I am attempting to model an existing C++ state machine.

Expected to get stuck on if(TimerGetElapsedTime(timeout_ref) >= IDLE_TIMEOUT, but instead I am stuck on just getting a valid transition.

Stripped down, I expect this model to step through Initialised -> Started -> Stopped.

It seems to go Initialised -> Stopped

What am I misunderstanding?

enum State { Initialised, Started, Stopped }

one sig A {
	var state: State
}

fact init {
	A.state = Initialised
}

pred skip { 
	A.state' = A.state
}

pred start {
	A.state = Initialised
	A.state' = Started
}

pred stop {
	A.state = Started
	A.state' = Stopped
}

fact step {
	always stop or start or skip
}

pred example { eventually A.state = Stopped }

run example
2

Mind the parentheses: it’s always (...). All unary operators bind tighter than binary ones.

1 Like