s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
3177 Commits
5 Branches
0 Tags
31 MiB
Tree: 3dd1680c6e
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '3dd1680c6e'
${ noResults }
Commit Graph

3177 Commits (3dd1680c6e984c89313db0ff1d9360de23af2954)
 

Author SHA1 Message Date
Joachim Klein 38617a9184 explicit: add support for CTL model checking
10 years ago
Joachim Klein 802abccbce explicit.StateValues: add complement() method (for boolean vectors)
10 years ago
Joachim Klein 5310be6b55 refactor SimpleLTL DAG check, remove common/PlainObjectReference.java
10 years ago
Joachim Klein 45b837567b explicit.CTMCModelChecker: fix handling of PCTL* subformulas
10 years ago
Joachim Klein 4dd6a008d4 explicit.StateModelChecker: handleMaximalStateFormulas by recursive checking and attaching labels to the model
10 years ago
Joachim Klein 2ea728c681 explicit.LTLModelChecker: accept any StateModelChecker (preparation for upcoming CTMC PCTL*-fix)
10 years ago
Joachim Klein 5cfe76d82a visitor.ReplaceLabels: for replacing labels in an expression
10 years ago
Joachim Klein 650e519e2d DTMCEmbeddedSimple: pass through label methods to underlying CTMC
10 years ago
Joachim Klein 19dd97cdd4 explicit: add ModelExplicit.addUniqueLabel() to help with attaching generated labels to a model
10 years ago
Joachim Klein 19a1111491 explicit: add Model.hasLabel() method
10 years ago
Joachim Klein ed0a08b00f explicit: Proper exception instead of null pointer exception for explicit with system definition
10 years ago
Joachim Klein faa8e1e51f ModulesFileModelGenerator: fix constant evaluation in explicit engine when built from GUI [with Steffen Maercker]
10 years ago
Joachim Klein e838330aae reapply previous commit (prepare prism-auto for python3 compatibility)
10 years ago
Joachim Klein e18c7362be temporarily reverting previous commit (to figure out some Jenkins build stuff)
10 years ago
Joachim Klein 4b711fe98a prism-auto: add parentheses for print call to make script compatible with python3
10 years ago
Joachim Klein da3761dd5d acceptance: add / cleanup complementation to AcceptanceGeneric
10 years ago
Joachim Klein dc5f714c1f AcceptanceRabin: fix name typo in complementation to Streett
10 years ago
Joachim Klein 3c564671f7 AcceptanceReach: Fix off-by-one bug in complementation to AcceptanceRabin
10 years ago
Joachim Klein 57258db7a2 typo: getListOfKeywords()
10 years ago
Joachim Klein 0cf8c8cbe0 GUI: Tweak double-click handling in property list
10 years ago
Joachim Klein 9ea440f147 GUI: In property editor dialog, place initial focus on the property text field
10 years ago
Joachim Klein 9e805295cc NBA: print(out, format) method, like for DA
10 years ago
Joachim Klein f9b84efc89 NBA: DOT output (roughly similar to the ltl2dstar DOT output)
10 years ago
Joachim Klein 17440416ca NBA: Fix HOA output (--END-- marker was emitted per state)
10 years ago
Dave Parker a89db49ecc Bug fix for use of model generators in Prism: PTA digital clocks + explicit engine was broken.
10 years ago
Dave Parker e2074832df Switch from ModuleFile to ModelInfo in Values object.
10 years ago
Dave Parker efbeda6faf Switch from ModuleFile to ModelInfo in State object.
10 years ago
Dave Parker 8c26fba334 Code tidy.
10 years ago
Joachim Klein f78b3437d6 ModelInfo: provide getVarIndex() and getVarName()
10 years ago
Dave Parker b6828a7045 Remove unused "techLog" from Prism object and other classes.
10 years ago
Vojtech Forejt 9b7737d1cc Changing an undocumented feature (aka bug) where in the output Pareto curve, probabilistic properties came before reward properties. Now the output respects the order which user gave on input to multi(...)
10 years ago
Vojtech Forejt 2d8194398b Fixed a bug where the type of multi was not correctly determined if boolean arguments came before double arguments. Now we enforce doubles to be given first.
10 years ago
Dave Parker 934e3f24e0 Bug fix in new ModelGenerator usage: breaks on existence of system...endsystem.
10 years ago
Vojtech Forejt f4961ba4ed Added an exception for the case when -lp is used for multi-objective, and there is a finite step bound. Up until now no warning was given and the step bound was ignored (treated as infinite)
10 years ago
Joachim Klein 04d1c3efdc StateModelChecker: remove mainLog field here, now stored in parent class PrismComponent
10 years ago
Joachim Klein 8d2199e0fe prism.StateModelChecker: initialise PrismComponent from other StateModelChecker constructor as well...
10 years ago
Dave Parker 5332421dff Comment typo.
10 years ago
Joachim Klein 9c1c80b2b0 prism.StateModelChecker: extends PrismComponent
10 years ago
Joachim Klein 6580cbdd79 PrismCL: Flush logfile on error
10 years ago
Vojtech Forejt 4562006bb0 fixed multiobjective lp bug where the reward objective function was not set if there were no PCTL targets.
10 years ago
Vojtech Forejt bd73bc0857 Minor stdout cleanup
10 years ago
Vojtech Forejt 5e935c3a35 Propagating bugfix from rev @11061 to Pareto curve generation
10 years ago
Dave Parker 85e6a903ba Bug fix: Value iteration multi-objective was removing self-loops in situations where it should not be.
10 years ago
Joachim Klein 303213e77b ProbModelChecker: Fix reference leak when doing steady-state computation (MTBDD)
10 years ago
Vojtech Forejt f0b5b2ca0c Bugfix for a case when the Pareto curve for minimising objectives contained (0,0) and the direction for a new hyperplane was not correctly computed
10 years ago
Vojtech Forejt efff3c629b Removing superfluous debugging output
10 years ago
Vojtech Forejt 563d0bd772 Added capability for testing Pareto curves (no tests added yet, and the Pareto curve generation itself is still buggy)
10 years ago
Dave Parker ccfaae3389 Add -exportmodeldotview switch (for now, hard-coded to use "dot" and "open" in path).
10 years ago
Dave Parker a025ae2e07 Add model checking of R[C] operator for CTMCs.
10 years ago
Joachim Klein ea537cc895 Expression.containsTemporalTimeBounds(): do not recurse into P/R/SS subformulas
10 years ago