19 commits

Author	SHA1	Message	Date
Adam Chlipala	ddacd030e6	Revising for Tuesday's lecture	2022-02-20 12:02:38 -05:00
Adam Chlipala	d3c7a85b49	More cleanup around addition of RuleInduction	2021-03-01 12:15:34 -05:00
Adam Chlipala	64fe989cdb	Turn off some warnings	2020-03-04 11:51:34 -05:00
Adam Chlipala	712aacf9de	Some ModelChecking improvements	2018-03-04 19:23:36 -05:00
Adam Chlipala	b0ad93e6a4	Fix up ModelChecking to track a change in TransitionSystems	2018-03-04 18:46:12 -05:00
Adam Chlipala	1e7c33f0a9	Optimizing tactics for faster state-space exploration	2017-03-05 20:46:53 -05:00
Adam Chlipala	b27e58f11e	Bump chapter numbers in Coq code comments	2017-02-21 09:00:30 -05:00
Peng Wang	f05378e111	Tweaked Ltac singletoner to display state space exploration in real time	2016-02-22 17:53:31 -05:00
Adam Chlipala	fd45f9d71a	Add ModelCheck	2016-02-21 12:16:31 -05:00
Adam Chlipala	211ede66a0	ModelChecking chapter done	2016-02-21 11:26:24 -05:00
Adam Chlipala	2b6ea9913c	Comments for ModelChecking	2016-02-21 09:07:14 -05:00
Adam Chlipala	2c601b04a0	Fixed to work in Coq 8.4, too	2016-02-18 17:51:58 -05:00
Adam Chlipala	d04037a84f	ModelChecking: an example of modularity	2016-02-16 11:17:50 -05:00
Adam Chlipala	e3bb90c4a1	ModelChecking: another abstraction example	2016-02-16 08:03:25 -05:00
Adam Chlipala	7aa8e890cf	ModelChecking: an example of abstraction	2016-02-15 21:20:54 -05:00
Adam Chlipala	c129d8447e	Some heftier ModelChecking examples	2016-02-14 19:23:26 -05:00
Adam Chlipala	eb50f67c2a	Smarter ModelChecking with a worklist	2016-02-14 17:55:59 -05:00
Adam Chlipala	4371d08696	Set simplification for ModelChecking	2016-02-14 17:33:46 -05:00
Adam Chlipala	c88ae6d484	Start ModelChecking code: checked [factorial_sys]	2016-02-14 17:13:25 -05:00