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

2308 Commits (7c65364af6dccaf8b12de1595ab35fac105e2c6c)

Author SHA1 Message Date
Dave Parker 5e92fabe95 Comment typo.
11 years ago
Dave Parker c5b40f44d8 Code tidy.
11 years ago
Dave Parker 32ad9bbaae Code tidy.
11 years ago
Dave Parker 3e990e89e3 Some tidying/fixing in EC generation, including proper support in the explicit engine version for finding ECs that intersect with "accept".
11 years ago
Dave Parker 53cb310c7a Code tidy.
11 years ago
Dave Parker 60a30d7038 Comment typo.
11 years ago
Dave Parker bb6693f43d Allow comments to have no trailing new-line (e.g. when occurring at very end of file) - cannot see a good reason not to allow this.
11 years ago
Dave Parker 9729c78b3e Inefficiency in precomputatino routines in explicit engine (spotted by Steffen Marcker).
11 years ago
Dave Parker a744b15a7e Fix (again) computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars).
11 years ago
Dave Parker 5557db131f Remove debug output.
11 years ago
Dave Parker 56e323a2b4 Fix computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars).
11 years ago
Dave Parker 9fc29a3b25 Bug fix in symbolic model checking of co-safe properties (target was not ANDed with reachable states).
11 years ago
Dave Parker 38f0e001c2 Bugfix in PrismParser.isKeyword (leading to incorrect identification of bad identifiers in SBML/reactions to PRISM translation).
11 years ago
Dave Parker b8fc45249e Added sbml2prism script.
11 years ago
Dave Parker 6a1417c6f4 Bug fix in explicit engine CTMC until model checking (spotted by Chris Dehnert) (probably due to recent ProbModelChecker refactoring).
11 years ago
Dave Parker 3b8d17c352 Missing toString in AcceptanceReach (and output tweak in DA).
11 years ago
Dave Parker 33ddccaf6b Add larger P icon (256x256).
11 years ago
Dave Parker ddeaef392e Exeutable bit on.
11 years ago
Dave Parker 0ae5d13247 Bug in building lp_solve_java on ia65 (from Alexandre Duret-Lutz).
11 years ago
Dave Parker cb294345ee CHANGELOG.
11 years ago
Dave Parker f7f4bf5f51 Model checkers: use DASimplify, allow AcceptanceReach in computations. [Joachim Klein]
11 years ago
Dave Parker ec4ddc4513 Add DASimplify. Currently supports simplifying DRA to DFA if the acceptance has a special form. [Joachim Klein]
11 years ago
Dave Parker c77bd235df Add AcceptanceReach, AcceptanceReachDD (for DFA style acceptance). [Joachim Klein]
11 years ago
Dave Parker d0384142bc LTLModelChecker: remove buildLStatesForRabinPair and buildKStatesForRabinPair, not needed anymore. [Joachim Klein]
11 years ago
Dave Parker 5b5bac7fe3 Adapt (symbolic) LTLModelChecker to support generic acceptance types for MDP. [Joachim Klein]
11 years ago
Dave Parker a16aeb57dc Adapt (symbolic) adapt LTLModelChecker to support generic acceptance types for DTMC. [Joachim Klein]
11 years ago
Dave Parker b6f3b2dce3 Adapt (explicit) LTLModelChecker to support generic acceptance types. [Joachim Klein]
11 years ago
Dave Parker f644011ba2 Refactor LTL-to-deterministic automaton generation, introduce LTL2DA and use LTL2RabinLibrary only for hard-coded and specially crafted DRA. [Joachim Klein]
11 years ago
Dave Parker 6ff3094b91 jltl2dstar: support generation of Rabin and Streett automata. [Joachim Klein]
11 years ago
Dave Parker 60ecccd9da New setting/switch: -pathviaautomata (all path formulas are handled via the LTL/DRA-engine), defaults to false. Honour in model checkers. [Joachim Klein]
11 years ago
Dave Parker 15a48d4fff LTLModelChecker.isSupportedLTLFormula(), for checking whether a path formula can be handled. [Joachim Klein]
11 years ago
Dave Parker e02281dc86 Add Expression.isPathFormula(). [Joachim Klein]
11 years ago
Dave Parker 9ad8e8165e LTL2RabinLibrary and model checkers: support automata based constructions for temporal bounds for simple path formulas. Now, the constantValues from the model checker have to be passed to LTL2RabinLibrary to allow resolving constants in the bounds. [Joachim Klein]
11 years ago
Dave Parker 441b278ed8 LTL2RabinLibrary: provide draForSimpleUntilFormula(), generating automata for a simple path formula with bounds. [Joachim Klein]
11 years ago
Dave Parker be5cdf908a Provide getConstantValues() for model checkers, allowing other classes to access the constants. [Joachim Klein]
11 years ago
Dave Parker d9ec3199b9 Refactoring: Expression.convertSimplePathFormulaToCanonicalForm(), converts to (negated) a U b or X a. Use in model checkers. [Joachim Klein]
11 years ago
Dave Parker a18d74e5b6 provide LTLModelChecker.constructProductMDP(MDP mdp, Expression ltl), encapsulating DA generation and product construction. [Joachim Klein]
11 years ago
Dave Parker e3ce1e85ee provide LTLModelChecker.constructProductMC(DTMC dtmc, Expression ltl), encapsulating DA generation and product construction. [Joachim Klein]
11 years ago
Dave Parker ab81007716 Lift stored labels and statelist to the product model. [Joachim Klein]
11 years ago
Dave Parker 36991a899a Refactor LTL product construction in explicit engine. [Joachim Klein]
11 years ago
Dave Parker 150775d09f Add ModelTransformation interface and abstract Product class for product of model and automaton. [Joachim Klein]
11 years ago
Dave Parker 5cd35caeda Missing adds/removes from last few commits
11 years ago
Dave Parker c00ffea7d8 Refactor: switch from prism.DRA<BitSet> to prism.DA<BitSet, AcceptanceRabin>. Changes access to the Rabin pairs. [Joachim Klein]
11 years ago
Dave Parker 02aa30d5bf Use AcceptanceRabin internally in prism.DRA. [Joachim Klein]
11 years ago
Dave Parker ad6c3b4800 Add acceptance.* package, with AcceptanceOmega and derived classes for BitSet-based acceptance and AcceptanceOmegaDD for JDD-based acceptance. [Joachim Klein]
11 years ago
Dave Parker 7e6f8e8cf6 Revert recent DFA optimizations to allow for acceptance type refactoring. Functionality will be later readded using AcceptanceReach. [Joachim Klein]
11 years ago
Dave Parker 4849d6d603 Remove check for lower bounds in path formulas for DTMC, MDP. [Joachim Klein]
11 years ago
Dave Parker 5dc15ad61b update checkProbBoundedUntil() in the model checkers to handle lower bounds as well. [Joachim Klein]
11 years ago
Dave Parker e77138a79f computeRestrictedNext() for ProbModelChecker, NondetModelChecker, DTMCModelChecker and MDPModelChecker. [Joachim Klein]
11 years ago
Dave Parker b8f6644f53 IntegerBound class for convenient handling of lower/upper bounds and intervals. [Joachim Klein]
11 years ago