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

2915 Commits (28f66c6c695a861c198031faf50ab7aa5de399e6)

Author SHA1 Message Date
Joachim Klein 28f66c6c69 BigRational: extend static BigRational from(Object value) to accept String value
10 years ago
Joachim Klein 8b569b9e4e BigRational: Make the static final constants (ONE, INF, NAN, etc) public
10 years ago
Joachim Klein 1f9fb4d505 BigRational: When canceling, preserve NaN instead of converting to ZERO
10 years ago
Joachim Klein 97c72b534e prism.UndefinedConstants: provide additional method removeConstants(Collection<String> constNames)
10 years ago
Dave Parker 7e51a56157 Code tidy
10 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
Joachim Klein ee4f2d2941 ExpressionTemporal: static constructors for the temporal operators
10 years ago
Joachim Klein 04bf278fd3 ExpressionTemporal: add Javadoc comments, fix getNumOperands() (is not used)
10 years ago
Joachim Klein f64be5223a ExpressionTemporal: convenience methods for testing for the various top-level temporal operators
10 years ago
Joachim Klein 7317c5f066 add jltl2ba.MyBitSet.clone()
10 years ago
Joachim Klein a4536fef48 add NBA.getSuccessors
10 years ago
Joachim Klein 3d51fd0f8f ExpressionUnaryOp, ExpressionBinaryOp: setOperator from symbol (string), for convenience
10 years ago
Joachim Klein c076b3e005 explicit.ModelTransformation: remove unnecessary Exception [from Steffen Märcker]
10 years ago
Joachim Klein 9a2d757554 explicit.ConstructRewards: error on negative rewards, use automatic close for BufferedReader
10 years ago
Joachim Klein 3d1ee7a66f LTL2DA.convertLTLFormulaToDAWithExternalTool: honor PRISM_NO_DA_SIMPLIFY setting
10 years ago
Joachim Klein 5c68cf3c2b param.BigRational: fix BigRational.MONE definition
10 years ago
Joachim Klein 494f61adeb PrismSTPGAbstractRefine: cleanup refactoring from SVN 11747
10 years ago
Joachim Klein 890620fd5f PrismSTPGAbstractRefine: set initial states from the label file
10 years ago
Joachim Klein 0667019a05 explicit: Make calls to StateModelChecker.loadLabelsFile static
10 years ago
Joachim Klein 55c0034a18 explicit model import: some more minor fixes to set correct initial states
10 years ago
Dave Parker a6eb2bd327 Add support for a state rewards file when doing explicit model import (not the explicit engine).
10 years ago
Dave Parker 81451753d1 Bug fix for explicit engine model import - we should not assume that the initial state is 0. This also highlights a bug that ModelExplicit should store initial states as a state, not a list, but that issue is not fixed here.
10 years ago
Dave Parker 0f9dfe0275 prism-auto: Make sure nailgun is closed down if the script ends with an error (and refactor the exit code).
10 years ago
Dave Parker 2a38cf110b prism-auto: Don't actually execute nailgun commands in echo mode - just print them.
10 years ago
Joachim Klein 5ae882f609 prism.ExplicitFiles2MTBDD: better I/O error messages
10 years ago
Joachim Klein 19cb2b45b5 arser.ExplicitFiles2ModulesFile: create label definitions in the ModulesFile for all labels in .lab file [with Steffen Maercker]
10 years ago
Joachim Klein 7d9beeaf21 ExplicitFiles2MTBDD/import: fully load label information and attach to model [with Steffen Maercker]
10 years ago
Joachim Klein 5fc4ca16ef symbolic models: allow attaching label state sets directly to the model (similar to explicit models)
10 years ago
Joachim Klein 2d494dbeac prism.ExplicitFiles2MTBDD: tidy JavaDoc, auto-close BufferedReaders [with Steffen Maercker]
10 years ago
Joachim Klein ef71f87d58 parser.ExplicitFiles2ModulesFile: automatic close for BufferedReader
10 years ago
Joachim Klein d9a0216159 parser.ExplicitFiles2ModulesFile: make PrismComponent (tidy)
10 years ago
Joachim Klein 76bf167c8e Prism: activate model import from explicit files for the explicit engine (-import... switches)
10 years ago