Insufficient tactic of `model_check_done` in FrapWithoutSets.v.
Closed this issue · 3 comments
Hi, I am trying to solve pset5 (producer-consumer formal verification) of 6.887 with transition system abstraction and model checking.
Looks like the tactic model_check_done
in FrapWithoutSets.v is insufficient to directly prove the abstracted transition system via model_check_infer
.
I make some hacks to change the tactic
Ltac model_check_done :=
apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
into
Ltac model_check_done :=
apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; apply sets_equal; simplify; propositional ].
And then model_check_infer
could just work.
My Coq (8.6) code for pset5 is here (deleted to avoid cheater). It takes about 1 minute to execute. You can just focus on L210 to L213. If I use the above hacks, L211 to L213 can be omitted.
As I am a really Coq novice, I don't understand some details of your Coq Ltac magic, can you figure out more details to check if it is a bug? Thanks.
Thanks for your interest in the book! First, to avoid creating a resource for students to cheat on this assignment in the future, could you please remove this solution and any others for our exercises from publicly accessible URLs? I've already saved your file for my own reference.
Aha, done.
Thanks. I just pushed a different small change that also fixes your problem, based on what I thought was the more fundamental issue with the FRAP tactics.