syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

verify request/response property in leader-and-seller

This commit is contained in:
Sam Caldwell 2019-09-26 13:39:25 -04:00
parent 2fa30c6066
commit 33b516b7a6
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
racket/typed/leader-and-seller.pml
View File

@ -163,6 +163,10 @@ ltl sanity {
BoTM_assertions >= 0)
&&
<> (BQ_assertions > 0)
&&
[] (ASSERTED(IBQ) -> <> ASSERTED(BQ))
&&
[] (ASSERTED(IBI) -> <> ASSERTED(BI))
/*
&&
<> (leader_state == announce || leader_state == none)