Removed doc text files (now in manual).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2409 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/NOTES-PTAS.txt

@@ -1,36 +0,0 @@
-Brief notes on support for PTAs in PRISM
-----------------------------------------
-
-* The PRISM Language
-
-In short, there is a new datatype "clock", which can be used in guards and reset (to an integer value) just like a normal PRISM variable. The only other addition is an "invariant" keyword, used to specify clock invariants for each PRISM module. The invariant should appear between the variable declarations and the guarded commands.
-
-In guards or invariants, references to clocks must be conjunctions of simple clock constraints (i.e. x~c or x~y where x and y are clocks, c is an integer-valued expression and ~ is one of <, <=, >=, >, =). In fact, when using the digital clocks method (see below), this is relaxed and boolean combinations of clock constraints are allowed.
-
-There are also some additional restrictions for PTA models. Modules cannot read the local variables of other modules and global variables are not permitted. The model must also have a single initial state (i.e. the init...endinit construct is not permitted). Again, when using digital clocks, the latter constraint does not apply.
-
-Model checking requires several assumptions: we require PTAs to be well-formed and non-zeno (see e.g. [KNP09c] for details). Currently, PRISM does not check automatically that these assumptions are satisfied.
-
-PRISM does check for timelocks, i.e. states in which it possible to get to a point where no transitions are available and time cannot elapse due to invariant conditions.
-
-There are a set of PRISM PTA examples in the directory examples/pta. See the formats09.sh script in this directory for details of how to run the examples.
-
-* 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 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. Also, the simulator does not yet support PTAs.
-
------------------
-
-[KNP09c]
-M. Kwiatkowska, G. Norman, and D. Parker.
-Stochastic games for verification of probabilistic timed automata.
-In Proc. FORMATS’09, volume 5813 of LNCS, pages 212–227. Springer, 2009.
-
-[KNPS06]
-M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston.
-Performance analysis of probabilistic timed automata using digital clocks.
-Formal Methods in System Design, 29:33–78, 2006.

prism/NOTES-STATMC.txt

@@ -1,41 +0,0 @@
-Notes on the new approximate/statistical model checking support in PRISM
-
-Previously, PRISM only supported a single kind of approximate/statistical model checking, namely checking of quantitative (e.g. P=?[...]) properties using the APMC method. Now, it offers four methods in total:
-
-* CI (Confidence Interval)
-* ACI (Asymptotic Confidence Interval)
-* APMC (Approximate Probabilistic Model Checking)
-* SPRT (Sequential Probability Ratio Test)
-
-and these can also be applied to bounded (e.g. P<p[...]) properties. SPRT is only applicable to bounded properties. The default method used is CI (for quantitative properties) and SPRT for bounded properties.
-
-Precise details of these methods can be found in the MSc thesis of Vincent Nimal:
-http://www.prismmodelchecker.org/bibitem.php?key=Nim10
-who worked on the code for this extension of PRISM.
-
-A brief guide to enabling the various new options from the command-line is as follows.
-(See also prism -help for a quick list.)
-
-* Switch -sim means that any model checking is done using approximate/statistical methods.
-
-* Switch -simmethod <name> selects the method to use: one of apmc, ci, aci, sprt.
-  The default is ci (Confidence Interval).
-
-* These methods share several parameters, configurable as follows:
-  - simsamples <n> - sets the number of sample paths generated for CI/ACI/APMC
-  - simconf <x> - sets the confidence (a probability) for CI/ACI/APMC
-  - simwidth <x> - sets the (half)-width of the confidence interval for CI/ACI
-  - simapprox <x> - sets the approximation size for APMC
-  Each of CI/ACI/APMC has three parameters which are related so you can set at most two.
-  For APMC, the third parameter can be computed immediately; for CI/ACI, this is done after simulation.
-  SPRT has three parameters: the acceptable probability of Type I and II errors,
-  and the 'indifference' parameter. The first two are both set with -simconf, the third with -simwidth.
-
-* Switch -simpathlen <n> sets the maximum length of paths generated by the simulator.
-
-* Switches -simmanual, -simvar <n> and -simmaxrwd <x> refer to technical details
-  described in Vincent's thesis and can be ignored for now.
-
-From the GUI, the mostly commonly used options can be set from the "Simulation Parameters"
-which appears when performing approximate model checking.
-The remaining options can be found in the "Simulator" tab of the "Options" dialog.