From dd26769b2e64408c2029dfdc222da39265a6f227 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 21 Jan 2010 20:36:05 +0000 Subject: [PATCH] Some tidying of PTA examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1691 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/examples/pta/simple/auto | 3 +++ prism/examples/pta/simple/{formats.nm => formats09.nm} | 3 +-- prism/examples/pta/simple/formats09.pctl | 3 +++ 3 files changed, 7 insertions(+), 2 deletions(-) create mode 100755 prism/examples/pta/simple/auto rename prism/examples/pta/simple/{formats.nm => formats09.nm} (72%) create mode 100644 prism/examples/pta/simple/formats09.pctl diff --git a/prism/examples/pta/simple/auto b/prism/examples/pta/simple/auto new file mode 100755 index 00000000..bad47d26 --- /dev/null +++ b/prism/examples/pta/simple/auto @@ -0,0 +1,3 @@ +#!/bin/csh + +prism formats09.nm formats09.pctl -prop 1 -aroptions refine=first diff --git a/prism/examples/pta/simple/formats.nm b/prism/examples/pta/simple/formats09.nm similarity index 72% rename from prism/examples/pta/simple/formats.nm rename to prism/examples/pta/simple/formats09.nm index ce249ba3..2d5c1c55 100644 --- a/prism/examples/pta/simple/formats.nm +++ b/prism/examples/pta/simple/formats09.nm @@ -8,8 +8,7 @@ module M x : clock; y : clock; - //[] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2)&(x'=0); - [] s=0 -> 0.3 : (s'=1) + 0.3 : (s'=1) + 0.2 : (s'=2)&(x'=0) + 0.2 : (s'=2)&(x'=0); + [] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2)&(x'=0); [] s=1 & x=0 -> (s'=3); [] s=1 & y>2 -> (s'=1)&(y'=0); [] s=2 & x=0 & y=1 -> (s'=3)&(y'=0); diff --git a/prism/examples/pta/simple/formats09.pctl b/prism/examples/pta/simple/formats09.pctl new file mode 100644 index 00000000..bc96bfc5 --- /dev/null +++ b/prism/examples/pta/simple/formats09.pctl @@ -0,0 +1,3 @@ +Pmax=? [ F "target" ] + +// Rmin=? [ F "end" ]