15 lines
No EOL
315 B
Text
15 lines
No EOL
315 B
Text
MODULE main
|
|
VAR
|
|
request: boolean;
|
|
status: {ready, busy};
|
|
ASSIGN
|
|
init(status) := ready;
|
|
next(status) := case
|
|
request: busy;
|
|
TRUE: {ready, busy};
|
|
esac;
|
|
|
|
LTLSPEC
|
|
G(request -> F status=busy)
|
|
LTLSPEC
|
|
G(request -> F status=ready) |