From 8c88d62b6f9f9b4b189104b4275541ca4c062d1e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 20 Jun 2012 09:20:27 +0000 Subject: [PATCH] Small tweak to firewire_abst model: unneeded invariant. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5374 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/pta/firewire/abst/firewire.nm | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/prism-examples/pta/firewire/abst/firewire.nm b/prism-examples/pta/firewire/abst/firewire.nm index 7da608a9..e5083261 100644 --- a/prism-examples/pta/firewire/abst/firewire.nm +++ b/prism-examples/pta/firewire/abst/firewire.nm @@ -43,8 +43,7 @@ module abstract_firewire (s=5 => x<=rc_fast_max) & (s=6 => x<=rc_slow_max) & (s=7 => x<=rc_slow_max) & - (s=8 => x<=rc_slow_max) & - (s=9 => x<=0) + (s=8 => x<=rc_slow_max) endinvariant // start_start (initial state)