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

3179 Commits (62f1e7d0acb34e5041a33cd000304cf3e9e7162c)
 

Author SHA1 Message Date
Joachim Klein 937a6c2a43 VarList: add getIndexFromDeclaration()
9 years ago
Joachim Klein 994b6207d9 AcceptanceGeneric: add toRabin() and toStreett() methods
9 years ago
Joachim Klein 30ed75086f AcceptanceGeneric: add and() and or() methods
9 years ago
Joachim Klein 16bbd0b24b Prism: reset currentModel and currentModelExpl to null in clearBuiltModel()
9 years ago
Joachim Klein 3d48780b8d Refactor: Switch MTBDD variable handling for symbolic models to ModelVariablesDD infrastructure
9 years ago
Joachim Klein a69f3d2e3f prism/ModelVariablesDD: for handling the MTBDD variable related logic for symbolic models
9 years ago
Joachim Klein 0fb6ab0a53 JDDVars: add mergeVarsFrom(), sortByIndex() and removeVar() methods
9 years ago
Joachim Klein 8b07176df3 ModelGenerator2MTBDD: simplify reference handling, use JDDNode.copy(), JDD.DerefArray()
9 years ago
Joachim Klein 410b38ab30 Modules2MTBDD: simplify reference handling, use JDDNode.copy(), JDD.DerefArray()
9 years ago
Joachim Klein 4340969f70 JDD: Add DerefArray convenience method
9 years ago
Joachim Klein d7c915394c JDDVars: deprecate addVars() and refAll(), instead use copy() or copyVarsFrom()
9 years ago
Joachim Klein c8d545b4f2 ast.RelOp: for negate, optionally keep the strictness of the operator [with Steffen Maercker and Marcus Daum]
9 years ago
Joachim Klein f54feb473b symbolic ProbModel: add method addUniqueLabelDD()
9 years ago
Joachim Klein 502faa6a26 explicit/symbolic: refactor checkExpressionLabel to use getLabelList()
9 years ago
Joachim Klein b80f41d5bc ModelExplicit: refactor addUniqueLabel to ensure that already defined label names are avoided
9 years ago
Joachim Klein 5a06f212a5 explicit/symbolic StateModelChecker: add methods getLabelList() and getDefinedLabelNames() to provide access to label namespace
9 years ago
Joachim Klein eb5028dbf8 prism-auto: add --dd-warnings mode for printing the CUDD reference leak warnings
9 years ago
Dave Parker 6bc5aefa50 Extend ModelGenerator2MTBDD to generate/store label info too.
9 years ago
Dave Parker a7efdff3ca Ignore "deadlock" label when loading from explicit files into symbolic engines (consistent with recent update to explicit engine import).
9 years ago
Dave Parker 3f7c3c57c8 Comment typo
9 years ago
Dave Parker 79ce4075b3 Add a default implementation of ModelInfo.rewardStructHasTransitionRewards in DefaultModelGenerator (which returns true), plus some notes about this in the JavaDoc for related methods.
9 years ago
Dave Parker a2ab087a55 Explicit model import via the explicit engine now respects the "fix deadlocks" setting and adds self-loops in deadlock states if needed.
9 years ago
Dave Parker f1ce3e4fa8 Unbreak ModelGenerator2MTBDD: max number of nondet choices had been set to 1 for testing purposes.
9 years ago
Joachim Klein e113bff2c7 ModelInfo: add method to query the existence of transition rewards, add check for explicit DTMC/CTMC reward construction
9 years ago
Dave Parker 002257286d Align parametric model construction with the non-parametric a little more.
9 years ago
Joachim Klein 048017bb24 NondetModelChecker.checkExpressionMultiObjective(): BDD cleanup when computeMultiReachProbs throws Exception
9 years ago
Joachim Klein 28f66c6c69 BigRational: extend static BigRational from(Object value) to accept String value
9 years ago
Joachim Klein 8b569b9e4e BigRational: Make the static final constants (ONE, INF, NAN, etc) public
9 years ago
Joachim Klein 1f9fb4d505 BigRational: When canceling, preserve NaN instead of converting to ZERO
9 years ago
Joachim Klein 97c72b534e prism.UndefinedConstants: provide additional method removeConstants(Collection<String> constNames)
9 years ago
Dave Parker 7e51a56157 Code tidy
9 years ago
Dave Parker 544c1cbe65 Missing part of previous bigfix.
10 years ago
Dave Parker 19ec2f0a76 Refactor parametric model construction to use an extension of ModelGenerator instead of reading specifically from a ModulesFile. Needs further refactoring.
10 years ago
Dave Parker 4f491f9e07 Bug fix in test mode comparisons where expected result is an expression comprising a single constant.
10 years ago
Dave Parker 37543a928d Bug fix in test mode comparisons where expected result is an expression comprising a single constant.
10 years ago
Dave Parker f4bae778ce Bug fix in test mode comparisons where expected result is an expression comprising a single constant.
10 years ago
Joachim Klein d126a8ae21 prism/Makefile: remove lib/prism.jar on clean
10 years ago
Joachim Klein 5fcf8f50e6 Makefile: compile ngprism with CFLAGS instead of CPPFLAGS options (calls C compiler)
10 years ago
Joachim Klein 72d08b9407 hybrid engine: consistently use delete[] when destroying solution vectors
10 years ago
Joachim Klein 9850ae3c71 sparse engine: consistently use delete[] when destroying solution vectors
10 years ago
Joachim Klein 08482e9f0d ExpressionReward: provide static variants of getRewardStructByIndexObject and getRewardStructIndexByIndexObject
10 years ago
Joachim Klein 6935798edf explicit.ProbModelChecker: provide constructRewards(model, rewardStructureIndex)
10 years ago
Dave Parker 9890d74315 Various improvements focused on the ModelGenerator interface:
10 years ago
Dave Parker 4ad8e43e9f Deal with module/model alphabets properly in PTAs, in particular when storing PTAs internally using pta.PTA. The definition of the alphabet of a PTA from a PRISM model is now correct and inline with the defition for other models.
10 years ago
Joachim Klein e38ea63e89 Fix U>=t computations for CTMC, explicit engine [with Marcus Daum]
10 years ago
Dave Parker 7615d9fcd8 Fix handling of PRISM_DEBUG and PRISM_DEBUG_ARG variables in launch scripts so that the scripts work when they are not set.
10 years ago
Dave Parker 241547abe9 Add PRISM_DEBUG and PRISM_DEBUG_ARG variables to launch scripts, which allow debugging of C++ code, as described at http://www.prismmodelchecker.org/wiki/Developers/Debugging.
10 years ago
Joachim Klein 338ef64bb6 Revert SVN 11756 "add jltl2ba.MyBitSet.clone()", breaks LTL->NBA generation
10 years ago
Dave Parker 3b68b5e0a9 Bug fix: respect disable_selfloop setting during adversary generation in LP-based multi-objective model checking.
10 years ago
Joachim Klein 3b4cb29c2c parser.Values: use PrismUtils.formatDouble for double formatting
10 years ago