15 lines
315 B
Text
15 lines
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)
|