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

2705 Commits (5156f2d9c573fbea472d165d329da885547246bf)
 

Author SHA1 Message Date
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
Dave Parker 8dbdce2e91 Test code for LTL formulas in PrismParser.
10 years ago
Dave Parker 7da07f7b99 Small refactor in positive normal form conversion.
10 years ago
Dave Parker 0c2e16ec32 Add conversion to positive normal form for LTL as well as boolean expressions.
10 years ago
Joachim Klein 6f8b090ef0 Settings: remove debug output for -ltl2datool argument
10 years ago
Dave Parker e140741c0a Remove unused method from BooleanUtils.
10 years ago
Joachim Klein f1aa7edc01 dv.cc/iv.cc: When converting from an MTBDD, check that we don't write outside of the DoubleVector/IntegerVector
10 years ago
Dave Parker d791bce62f Add some more options to LTL2DA program
10 years ago
Dave Parker 6e5a62eb42 Add some more options to LTL2DA program
10 years ago
Dave Parker 7f6c068e8b Add a simple command-line test program (LBT->HOA) to LTL2DA.
10 years ago
Dave Parker 5145992646 Bug fix in Expression.isPositiveNormalFormLTL: do not assume type checking has already been done.
10 years ago
Dave Parker 81f73d19d7 Bugfix in new SimpleLTL-to-Expression method.
10 years ago
Dave Parker fe305344df Utility function to create an Expression from an LTL formula represented as a jltl2ba SimpleLTL object (i.e., the reverse of Expression.convertForJltl2ba()).
10 years ago
Dave Parker ad238d314c Allow -exportpropaut to export DA in HOA format, e.g.: prism dice.pm -pf "P=?[X X d=6]" -exportpropaut:hoa da.hoa
10 years ago
Joachim Klein c79a27b218 HOAF2DA: add main() method to provide command-line interface for testing deterministic HOA parsing.
10 years ago
Joachim Klein fd46caec64 Add Jltl2dstarCmdLine command-line interface for LTL -> DRA functionality (for testing)
10 years ago
Joachim Klein 449b06ef8f Add Jltl2baCmdLine command-line interface for LTL -> NBA functionality (for testing)
10 years ago
Joachim Klein b1863bb528 automata.DA: printHOA()
10 years ago
Joachim Klein f449803020 Acceptance: add outputHOAHeader()
10 years ago
Joachim Klein 4bd03ef854 Acceptance: add getSignatureForStateHOA()
10 years ago
Joachim Klein 5cafc40cb9 AcceptanceGeneric: add missing getSignatureForState() functionality
10 years ago
Joachim Klein 1a17950deb AcceptanceGeneric: add getLoafNodes() helper
10 years ago
Joachim Klein 96600e7a2f jltl2dstar.DA: printHOA
10 years ago
Joachim Klein 490642291d jltl2dstar.DA: fix print (ltl2dstar format output)
10 years ago
Joachim Klein 80a78f9ec5 jltl2dstar.NBA: printing in LBTT and HOA format
10 years ago
Joachim Klein 6d3bfff9a6 jltl2ba.APElement: printing in LBTT / HOA format
10 years ago
Joachim Klein 5d3adc211c jltl2ba.APSet: add print_hoa()
10 years ago
Joachim Klein ca47143da5 SimpleLTL: add parsing functionality for LBT(T) formulas (prefix format)
10 years ago