pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of github.com:achlipala/frap

Browse source
This commit is contained in:
Adam Chlipala 2021-01-03 14:56:48 -05:00
commit 5376847d16
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
MessagesAndRefinement.v
View file

@ -202,7 +202,7 @@ Definition simulates (R : proc -> proc -> Prop) (pr1 pr2 : proc) :=
-> exists pr2', lstepSilent^* pr2 pr2' -> exists pr2', lstepSilent^* pr2 pr2'
/\ R pr1' pr2') /\ R pr1' pr2')
(* Now consider the same scenario where the lefthand process make a nonsilent (* Now consider the same scenario where the lefthand process takes a nonsilent
* step. We require that the righthand process can "catch up" in a way that * step. We require that the righthand process can "catch up" in a way that
* generates the same label that the lefthand process generated. *) * generates the same label that the lefthand process generated. *)
/\ (forall pr1 pr2, R pr1 pr2 /\ (forall pr1 pr2, R pr1 pr2