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

3032 Commits (3d72a13cc3f30336558cecacca4334c028117b58)
 

Author SHA1 Message Date
Dave Parker 4ee20e5583 Bug fix in lifting reward structures to a product model (when there are some states with no transition rewards).
10 years ago
Dave Parker c143d38707 Makefil fix: Pass location of ngprism for tests/testslocal targets.
10 years ago
Dave Parker b44b789235 Parent dir Makefile file.
10 years ago
Dave Parker 0b04c50ea5 Auto-format (for merging purposes).
10 years ago
Dave Parker 5ce657090b Make tool name ("PRISM") configurable.
10 years ago
Dave Parker b789d5ed56 Code tidy.
10 years ago
Dave Parker 4c88a8185c Generalise parent directory Makefile to allow easier building from PRISM extensions such as PRISM-games.
10 years ago
Dave Parker 7456dbf2fe CHANGELOG.
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).
10 years ago
Dave Parker 69b2ed1f08 Makefile tests targets use Nailgun.
10 years ago
Dave Parker ce6131636e Some refactoring of the RelOp and ModelType enums. [from Steffen Marcker]]
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).
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).
10 years ago
Dave Parker 7511a39939 Additional functionality in LTL parser test code.
10 years ago
Dave Parker 1097ecaaeb Add a second syntactic co-safe-ness check, which first converts to positive normal form.
10 years ago
Dave Parker 2c6fece3d9 Auto-format
10 years ago
Dave Parker f85e2cfa85 Remove some unnecessary exception throwing from functions in BooleanUtils.
10 years ago
Dave Parker f7e4b6f747 Comment typo
10 years ago
Dave Parker 7f3862e636 Minor refactoring (allow PrismLangException to thrown instead of PrismException). [from Steffen Marcker]
10 years ago
Dave Parker 31877c0f2d Small refactoring in DTMCExplicit: cleaner implementation of iterator.
10 years ago
Dave Parker b7f3871fd7 Fix for SCC export on MDPs (and new underlying methods for computing/storing transition relation).
10 years ago
Joachim Klein 7e28e62317 Refactor timeout: conversion in PrismUtils, now additionally supports days (d) and weeks (w) for long-term model checking
10 years ago
Dave Parker b7a034bb85 Remove changes accidentally commited in rev 10595.
10 years ago
Dave Parker fca843737f Frivolity reduction ;)
10 years ago
Joachim Klein 95fab44a03 First try at a timeout mechanism (undocumented at the moment) for command-line PrismCL.
10 years ago
Dave Parker 70a48835ad Bug fix in CNF conversion (from Yuyang).
10 years ago
Dave Parker 0f9e001645 Bug fix in CNF conversion (from Yuyang).
10 years ago
Dave Parker 5156f2d9c5 Fix in previous improvement to prism-auto.
10 years ago
Dave Parker 33e745af83 prism-auto: Location of ngprism can optionally be specified with --ngprism.
10 years ago
Dave Parker 6dd6628f52 Preliminary Nailgun support for prism-auto (add --nailgun).
10 years ago
Dave Parker 2026632c37 ngprism: Allow the use of "ngprism stop" to kill the server.
10 years ago
Dave Parker 0cc899aad4 ndprism executable: tidy Makefile and disable building on Windows (Cygwin) for now.
10 years ago
Dave Parker ff49cfd2a6 Add Nailgun jar, missing from last commit.
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.
10 years ago
Dave Parker 2119ef3f85 Slight tweak to LTL test in parser.
10 years ago
Joachim Klein eeddcf9039 Add hasTransitionRewards() method to explicit Reward interface.
10 years ago
Joachim Klein 5d33639dd7 explicit.LTLModelChecker: Comment whitespace
10 years ago
Joachim Klein 423d169552 Symbolic LTLModelChecker: Provide constructDAForLTLFormula, use in ProbModelChecker and NondetModelChecker
10 years ago
Joachim Klein 298266c1cd explicit.LTLModelChecker: construct a VarList for the Model-DA product if the model had a varlist
10 years ago
Joachim Klein 35461f5e2f explicit: setVarList() / getVarList() for the explicit models
10 years ago
Joachim Klein 7d049a979d PrismLog: implement Closable / AutoClosable [with Steffen Maercker]
10 years ago
Joachim Klein 152031aff5 Symbolic, BSCC computation: Omit BSCC size output when there are >10 BSCCs
10 years ago
Joachim Klein fd5c1c90d8 ECComputerDefault: optimize by using BitSet.isEmpty() instead of BitSet.cardinality() == 0
10 years ago
Joachim Klein 307e8b586f lpsolve5j.cpp: Fix deletes
10 years ago
Joachim Klein 3da87f5bf5 prism-auto: support multiple -x arguments
10 years ago
Dave Parker b4a1fc0b79 Code tidy (auto-format).
10 years ago
Dave Parker f4bc0ee72c Add equals and hashCode methods to Expression class hierarchy (Eclipse auto-generated).
10 years ago
Dave Parker a9456fa826 Code tidy.
10 years ago
Dave Parker 9493710a0f Add some additional functionality to the LTL test mode of PrismParser.
10 years ago
Dave Parker 0d5cc45f53 Bug fix in the check for syntactic co-safe LTL formulas: implication/iff not allowed.
10 years ago