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