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
14 years ago · 8c88d62b6f
1 changed files with 1 additions and 2 deletions
--- 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)