int main() { while (true) ; }
P is a liveness property,not P is not a safety property.
P is a safety property, not P is not a liveness property.
not.
P
P into the code so that every execution path
contains at least one instance of P.
P
can go anywhere.
P is true whenever execution hits it.
|
|
co < await even(i) ; S1 ; i++ > || < await odd(i) ; S2 ; i++ > oc
co < await i % 2 == 0 ; S1 ; i++ > || < await i % 3 == 0 ; S2 ; i++ > oc
{ LNP } S { post }
LNP is true sometime during execution
but not necessarily just before S is executed.
{ true } < await LNP ; S > { post }
S will not execute until LNP is true.
for i = 1 to n
while thread i has statements left
execute the next statement in thread i
Execute thread 1 to completion,
then execute thread 2 to completion,
then . . .
bool done = false co while (!done) skip || done = true oc
Thread 2 never executes and the computation never terminates
for i = 1 to n
if thread i statement is eligible
execute the statement
< await B ; s > is conditionally enabled on B.
co < await odd(i) ; S > || while (true) i++ oc
< await B ; S > is monotonic
if B, once true, stays true.
co < await odd(i) ; S > || while (true) i++ oc
This page last modified on 19 June 2003.