Dave Parker
be53bceb72
Rename a few visitor classes
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4502 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
fd968a89d1
Check for cyclic dependencies in property references.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4501 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
ac31984b5a
Fix type checking for property references (and some autoformatting - oops).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4500 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
c7365ce0d9
Bugfix: look for undefined constants recursively in referenced properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4499 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
c7d1af5f85
More fixes for bugs introduced in recent "improvements" to constant handling API:
- setSomeUndefinedConstants(null) call changed in PropertiesFile
- expandConstants() handles undefined constants cleanly
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4460 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Vojtech Forejt
e3f6e64e7a
package-info.java is ignored in makefiles
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4380 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
148f2b814e
Fix in numerical value comparison for -test checks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4310 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
086bb3243d
RESULT label for test properties can be NaN.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4305 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
854cd58edd
Typo in error message (old debugging info).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4250 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
95d7e89a57
Bugfix: previous "improvement" to API wrt undefined constants broke some models, e.g. when trying to evaluate pow/floor etc. with wrong number of arguments.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4249 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
7fda209763
Undo revision 4243 - alternative fix coming up
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4248 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Vojtech Forejt
b1ea8c04d4
Fixed handling of the case when functions like pow, floor, etc. are given incorrect number of arguments.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4243 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Vojtech Forejt
b1e27b40c5
added a missing class for handling named properties in the gui
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4114 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
a066e5db8e
Bugfix in handling of init/deadlock labels during constant processing - e.g. P=?[F "deadlock"&x=i] failed if i was a constant.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4085 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
bf59e25a49
Fixed a bug in getAllUndefinedConstantsRecursively. Showed up when running auto in embedded example. Bug found by Janne Kauttio.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3983 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
9e7ff7c43b
Makefile fix. Package parser.type may not get built in some scenarios.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3969 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
14025e109d
Improvements to StateValues class + it's use in explicit model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3581 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3e8f246006
Typos in javadoc comments.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3550 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3723afae6c
New isDefinedConstant methods (+ code tidy).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3437 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d4ce4fa73c
Code doc
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3380 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
10313b7d02
Improved handling of undefined constants in properties files:
* don't need to provide values for all constants, just those required for model checking
And a few related bug fixes:
* in error handling for constants in PrismCL
* in export of labels from properties file with constants
And some small related API changes:
* don't need to call setUndefinedConstants on ModulesFile/PropertiesFile if there are no undefined constants
* more flexible UndefinedConstants classes
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3319 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
36e523c90a
Bugfix: bug added in recent changes to initial state creation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3300 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
26130c8d38
Correct types for initial state of ModulesFile (only a problem when there are clocks).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3298 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
af6eef0c49
Added castValueTo method to Type classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3288 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
41f38a34fc
Added ability to have multiple RESULT test specifications for different constant values, e.g. "RESULT (x=1,y=2): 0.5".
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3285 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
f1bac71e5d
Improved doc for Values class + new toStringConcatenated method.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3284 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
cb49b36fc3
Bugfix: property handling in PTA model files fails (caused by inability to call tidyUp() twice in PropertiesFile).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3262 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
8bbda8f530
Added new expression evaluation methods (needed for explicit model checker). Unfortunately breaks some existing calls to evaluate(constVals, null) due to ambiguities. Need to replace them with evaluate(constVals).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3254 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
2654125531
* Check added to catch if the same variable is set twice in the same update
* New class of semantic checks created that are only done after constant definitions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3231 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d0d92d3dc9
Code documentation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3230 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
a126367821
Simulator engine: Documentation of Choice object, remove some unused Choice methods, add some action-querying methods in SimulatorEngine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3212 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
6289094aa0
Property references can appear in properties (still a few TODOs though).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3186 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
3c8ca8495d
Added iff (<=>) to PRISM model/properties language.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3175 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
8465fdeb07
Property names parsed (but not used) and -test switch added (but no property/verify blocks yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3096 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
4ad686212f
Bug fix in ExpandLabels: missing deepCopy (only affects explicit engine currently).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3095 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
ce4b0beb1e
Undoing last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3079 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
bcab165234
Use gcc-3 etc by default when building on Cygwin.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3078 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
be47ad30e8
Cleaner handling of model types in parser code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3042 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d6bc7b263d
ModulesFile: getRewardStructByName method + cmment tidies.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3041 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
71ca9d28af
Final (pre-4.0) fixes to filters: added "state" filter, which gives result for a filter which must satisfy exactly one state, and make this the translation for old-style {state} filter.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2910 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
087ea5da6a
General tidy up of initial state handling in simulator, including a few GUI bug fixes. GUI default is to use the default initial state. For generation of simulation paths, there is a separate menu item to start from a specified state (and no option to switch asking on/off). Additional tidying and documentation in related parts of code too.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2835 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
37a11d25bd
Parser accepts unicode (e.g. in comments).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2830 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
4e2df081a9
Added -css switch to prism2html to allow override of style file location.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2829 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
1e083eb20d
Missing/broken copyright headers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2490 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
35f377ab3e
Improved documentation (JavaDoc mostly).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2436 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
07098cca94
Fix: inter-module var access allowed for digitsal clocks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2421 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
53a5274cb3
Addition of new statistical model checking stuff (patch difference between trunk and prism-statmc branch at this revision).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2391 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
5dcbaab5eb
Header typo: author attrib.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2381 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
76d7039060
Code tidy: stop PrismExceptions on formula expansion (eases debugging) and remove an unused method.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2379 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
da822f4a6b
Code comments.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2378 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago