From 503854afac59e0cb4ac2e62999dcc89eb2a7b386 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 18 Mar 2008 17:08:01 +0000 Subject: [PATCH] Bug fix in phil_lss model. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@691 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/phil_lss/phil_lss3.nm | 2 +- prism-examples/phil_lss/phil_lss4.nm | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prism-examples/phil_lss/phil_lss3.nm b/prism-examples/phil_lss/phil_lss3.nm index 8365c802..a555dd15 100644 --- a/prism-examples/phil_lss/phil_lss3.nm +++ b/prism-examples/phil_lss/phil_lss3.nm @@ -57,7 +57,7 @@ endmodule // atomic formule // left fork and right fork free resp. formula lfree = p2>=0&p2<=4|p2=6|p2=11|p2=13; -formula rfree = p2>=0&p2<=3|p2=5|p2=7|p2=12|p2=13; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=12|p3=13; module phil1 diff --git a/prism-examples/phil_lss/phil_lss4.nm b/prism-examples/phil_lss/phil_lss4.nm index cc0e4fcd..fb61207b 100644 --- a/prism-examples/phil_lss/phil_lss4.nm +++ b/prism-examples/phil_lss/phil_lss4.nm @@ -84,7 +84,7 @@ endmodule // atomic formule // left fork and right fork free resp. formula lfree = p2>=0&p2<=4|p2=6|p2=11|p2=13; -formula rfree = p2>=0&p2<=3|p2=5|p2=7|p2=12|p2=13; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=12|p3=13; module phil1