-
Thanks for the report. This a manual bug - the use of ranges (e.g. 1..10) is no longer supported in new versions of PRISM.
See http://www.prismmodelchecker.org/language-changes.php for details.
I will update the manual.
Thanks,
Dave.
2009-10-20 20:34:51 UTC in The PRISM Probabilistic Model Checker
-
File Added: bug.csl.
2008-05-24 21:16:40 UTC in The PRISM Probabilistic Model Checker
-
Dave,
the properties should give the same answer as the variable is never decremented if it is greater than L before time T then it is greater than L at time T. In any case with L=0 both formulae should always hold with probability 1.
However running
prism bug.{sm,csl} -fixdl -const L=0,T=100,M=10 -sim -simsamples 100 -simpathlen 1000 | grep Res
returns
Result: 1.0
Result: 0.0...
2008-05-24 21:16:09 UTC in The PRISM Probabilistic Model Checker
-
Fixed as of version 3.2.
Dave.
2008-04-02 15:18:38 UTC in The PRISM Probabilistic Model Checker
-
Thanks again for the detailed info. I just repeated the test over ssh (-Y) between two Linux machines and observed no problems. So yes - this seems likely to be an X11/Java issue on Macs.
Thanks,
Dave.
2008-01-09 11:30:50 UTC in The PRISM Probabilistic Model Checker
-
Thanks for the report. I can't reproduce this though using recent versions of PRISM on my machines (Linux/Windows).
Could you please confirm which version of PRISM, which operating system and which version of Java you are using? Thanks.
2007-11-19 18:51:24 UTC in The PRISM Probabilistic Model Checker
-
Fixed 1/11/2007 (svn rev 502)
2007-11-01 15:11:43 UTC in The PRISM Probabilistic Model Checker
-
OK, this is due to a slight peculiarity in the PRISM property language: implication can appear in properties, but not in normal expressions, as appearing e.g. in PRISM models or atomic propositions/labels in properties files. Labels, which can be used in properties files, are in fact just a way of assigning names to expressions.
Hence,
label "Tautology" = (true)=>(true);
is not...
2007-10-02 13:36:48 UTC in The PRISM Probabilistic Model Checker
-
I am moving this discussion to the help forum and closing the bug...
Dave.
2007-10-01 12:59:04 UTC in The PRISM Probabilistic Model Checker
-
Implication (=>) _is_ allowed in properties. There is probably an issue with operator precedence. Try enclosing either side of the implication in brackets: (...)=>(...)
And yes this is missing from the property dialog, as are other things such as reward operators. This dialog is due to be redesigned some time soon...
Dave.
2007-10-01 12:57:51 UTC in The PRISM Probabilistic Model Checker
