From 16e4860ec3fb0d53ad06f57e0ce0d4dd00bface5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 1 Nov 2010 13:07:06 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2212 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 1 - prism/NOTES-PTAS.txt | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index 0694bdee..d7262ead 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -9,7 +9,6 @@ TODO (before any release) PTAs: * (Further) tidy of prism-examples/pta -* Check guards/invariants for convexity (for now, neither can be non-convex, see below) * Clarify time divergence issues * non-zeno checks? diff --git a/prism/NOTES-PTAS.txt b/prism/NOTES-PTAS.txt index 74e64616..1d166754 100644 --- a/prism/NOTES-PTAS.txt +++ b/prism/NOTES-PTAS.txt @@ -13,11 +13,11 @@ There are a set of PRISM PTA examples in the directory examples/pta. See the for * Properties -Properties are specified in PCTL, with no nested P operators, i.e. essentially we allow unbounded or time-bounded reachability properties: properties of the form Pmin=?[F a], Pmax=?[F a], Pmin=?[F<=T a] or Pmax=?[F<=T a], where a is a Boolean-valued expression, not including any clock variables. See the .pctl files included with the examples for some sample properties. For digital clocks, a few less restrictions are in place, e.g. until formulae are allowed, as are clock variables in expressions, as are arithmetic expressions such as 1-Pmin=?[F...]. +Properties are specified in PCTL, with no nested P operators, i.e. essentially we allow unbounded or time-bounded reachability properties: properties of the form Pmin=?[F a], Pmax=?[F a], Pmin=?[F<=T a] or Pmax=?[F<=T a], where a is a Boolean-valued expression, not including any clock variables. See the .pctl files included with the examples for some sample properties. For digital clocks, a few less restrictions are in place, e.g. until formulae are allowed, as are clock variables in expressions, as are arithmetic expressions such as 1-Pmin=?[F a]. * Running PRISM -Currently, there are two different engines for verifying PTAs: (1) "abstraction-refinement", as described in [KNP09c]; and (2) "digital clocks", as described in [KNPS06]. The default is (1). The digital clocks engine can be enabled using the switch "-ptamethod digital". Note, though, that this does not yet support time-bounded reachability properties. +Currently, there are two different engines for verifying PTAs: (1) "abstraction-refinement", as described in [KNP09c]; and (2) "digital clocks", as described in [KNPS06]. The default is (1). The digital clocks engine can be enabled using the switch "-ptamethod digital". Note, though, that this does not yet support time-bounded reachability properties. Also, the simulator does not yet support PTAs. -----------------