Dave Parker
|
85b7c30d4a
|
Catch possible null value in GUI simulator update table display (reported by Steffen Marcker).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10833 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
a64997f903
|
Bugfixes in sparse engine adversary generation (cumulative reward and multi-objective): remove second stat line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10831 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
91d984cce8
|
Add some adversary generation for multi-objective value iteration (just exports one adv for each separated weighted objective).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10829 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
3347d55d0a
|
Bug fix for updateAutoParse(): from prism-games.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10826 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
d4c5fd4fd5
|
Remove accidental commits
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10816 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
ff05caf158
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10815 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
cd859b45db
|
Multi-objective value iteration: generate (but do not yet export) adversaries for each weighted query.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10814 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
655cfb3550
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10813 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
09bebccb52
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10812 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
2806712f80
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10811 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
2de15e6b68
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10810 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
ec285b66b1
|
Some tidying in multi-objective code (auto format).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10809 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
e932ae1227
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10808 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
412ac91a61
|
Bug fix in multi-objective value iteration: non-convergence when one objective has weight 0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10806 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
91227cf4c8
|
Highlight some error messages in the Makefile (fix).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10790 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
3a104c0760
|
Highlight some error messages in the Makefile.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10788 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
bb67630285
|
Allow for modified tool name when printing version info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10777 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
ce6ffdcc13
|
Default format type for DA.print methods.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10755 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
4ee20e5583
|
Bug fix in lifting reward structures to a product model (when there are some states with no transition rewards).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10750 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
c143d38707
|
Makefil fix: Pass location of ngprism for tests/testslocal targets.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10728 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
0b04c50ea5
|
Auto-format (for merging purposes).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10717 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
5ce657090b
|
Make tool name ("PRISM") configurable.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10715 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
b789d5ed56
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10713 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
7456dbf2fe
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10688 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
f8e4f427bc
|
Refactoring of to-PRISM language translations: addition of PrismLanguageTranslator abstract class (preliminary version of) and connection with SBML/reactions/PEPA translators. Also, add support for SBML import to Prism class (but not used elsewhere yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10687 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
69b2ed1f08
|
Makefile tests targets use Nailgun.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10622 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
ce6131636e
|
Some refactoring of the RelOp and ModelType enums. [from Steffen Marcker]]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10616 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
11c1a65260
|
Allow wider ranger of co-safe LTL formulae inside an R operator (more precisely, those that can also be rewritten into co-safe form).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10614 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
04ba6cbe1e
|
Allow wider ranger of co-safe LTL formulae inside an R operator (more precisely, those that can also be rewritten into co-safe form).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10613 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
7511a39939
|
Additional functionality in LTL parser test code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10612 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
1097ecaaeb
|
Add a second syntactic co-safe-ness check, which first converts to positive normal form.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10611 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
2c6fece3d9
|
Auto-format
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10610 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
f85e2cfa85
|
Remove some unnecessary exception throwing from functions in BooleanUtils.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10609 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
f7e4b6f747
|
Comment typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10608 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
7f3862e636
|
Minor refactoring (allow PrismLangException to thrown instead of PrismException). [from Steffen Marcker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10606 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
31877c0f2d
|
Small refactoring in DTMCExplicit: cleaner implementation of iterator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10605 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
b7f3871fd7
|
Fix for SCC export on MDPs (and new underlying methods for computing/storing transition relation).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10604 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Joachim Klein
|
7e28e62317
|
Refactor timeout: conversion in PrismUtils, now additionally supports days (d) and weeks (w) for long-term model checking
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10603 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
b7a034bb85
|
Remove changes accidentally commited in rev 10595.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10599 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
fca843737f
|
Frivolity reduction ;)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10598 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Joachim Klein
|
95fab44a03
|
First try at a timeout mechanism (undocumented at the moment) for command-line PrismCL.
-timeout 5 5 seconds
-timeout 5s 5 seconds
-timeout 1m 1 minute
-timeout 1h 1 hour
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10597 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
70a48835ad
|
Bug fix in CNF conversion (from Yuyang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10596 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
0f9e001645
|
Bug fix in CNF conversion (from Yuyang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10595 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
5156f2d9c5
|
Fix in previous improvement to prism-auto.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10594 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
33e745af83
|
prism-auto: Location of ngprism can optionally be specified with --ngprism.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10593 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
6dd6628f52
|
Preliminary Nailgun support for prism-auto (add --nailgun).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10592 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
2026632c37
|
ngprism: Allow the use of "ngprism stop" to kill the server.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10591 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
0cc899aad4
|
ndprism executable: tidy Makefile and disable building on Windows (Cygwin) for now.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10590 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
ff49cfd2a6
|
Add Nailgun jar, missing from last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10589 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
3464a921ad
|
First version of Nailgun support built directly into PRISM. Adding switch -ng when running prism will instead start a Nailgun server ready to run PRISM instances, and running ngprism runs PRISM as a Nailgun client.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10588 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |