sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Commit Graph

  • bdb2aa8de9 fixed scheduler output hannah 2021-07-16 16:40:10 +0200
  • d7b696a753 restructured the ltl-scheduler hannah 2021-07-15 20:21:00 +0200
  • dd8d410748 updated scheduler-print and tests hannah 2021-07-12 10:20:39 +0200
  • 93c2e92c2a updated LTL-scheduler hannah 2021-07-11 03:01:58 +0200
  • 0983f2f564 print memory updates hannah 2021-07-11 03:01:25 +0200
  • 49e346d52b new Test hannah 2021-07-07 17:55:01 +0200
  • 991cf35f2f print memoryStructure hannah 2021-07-05 13:05:50 +0200
  • 08c454f124 scheduler support for LTL-MC hannah 2021-07-05 12:38:12 +0200
  • f596d7f486 fixed output hannah 2021-07-05 09:23:01 +0200
  • 7455bd8e00 add missing include Tim Quatmann 2021-07-01 12:29:43 +0200
  • 113f17372f set hasQualitativeResult to false for HOAFormulas hannah 2021-06-29 08:19:22 +0200
  • 5cc5057cd6 removed unused function hannah 2021-06-28 07:56:49 +0200
  • b49837eb4e use LTLHelper to compute HOAPath Formulas hannah 2021-06-27 16:22:00 +0200
  • a88b64bad3 DTMC HOA tests hannah 2021-06-27 15:14:41 +0200
  • 97c3bdd5a7 HOA Formula Parser Tests hannah 2021-06-27 13:35:55 +0200
  • 4655dc19a1 fixed MDP-LTL test hannah 2021-06-23 14:22:55 +0200
  • d21d2ca7e6 fixed exceptions hannah 2021-06-23 09:24:34 +0200
  • ca6b3b8ce2 missing include hannah 2021-06-23 08:44:19 +0200
  • 4cdd70949c FormulaParser: HOA formulas shall only consider state-subformulas Tim Quatmann 2021-06-23 06:27:54 +0200
  • bf3894d2f8 DA state output hannah 2021-06-20 16:05:29 +0200
  • 57734226e2 channged data structure for extracted formulas hannah 2021-06-18 13:52:51 +0200
  • 71f72d84b2 Ma ltl-MC and tests hannah 2021-06-18 12:29:24 +0200
  • 225169b2b3 added ltl2da option hannah 2021-06-18 09:24:39 +0200
  • 1d5860de8d use same labels for equivalent maximal state formulas hannah 2021-06-17 18:52:40 +0200
  • 75ddf49f2b compute SatSets via LTLHelper hannah 2021-06-17 13:23:38 +0200
  • ecd4637df3 AP simplifications in LTL-Formula hannah 2021-06-15 21:45:56 +0200
  • 1332e39b8c updated canHandle hannah 2021-06-15 21:44:52 +0200
  • b75c16297f fixed some typos hannah 2021-06-15 10:39:49 +0200
  • 8ba4f17a92 ltl-mc with MAs hannah 2021-06-13 18:53:46 +0200
  • 78058b5152 ltl-mc with ctmcs hannah 2021-06-13 18:47:33 +0200
  • 7f95f1fdbf ctmc and mdp tests hannah 2021-06-13 18:40:31 +0200
  • a038d9658e added TODOs hannah 2021-06-13 18:39:00 +0200
  • b06151b913 ctmc-ltl tests hannah 2021-06-09 23:23:13 +0200
  • 3f030e23f0 allow external ltl2da tools hannah 2021-06-09 23:14:24 +0200
  • ca4ac3a166 transform into generalized Rabin instead of DNF hannah 2021-06-06 21:01:58 +0200
  • e838ac13de updated ltl tests hannah 2021-05-26 15:18:16 +0200
  • 667d4a0e06 documentation and renaming of some methods hannah 2021-05-26 12:44:07 +0200
  • 139ac3d0dc flag to indicate whether condition should be in dnf hannah 2021-05-26 12:39:19 +0200
  • 93d9b586ed compute 1-Pmax[in order to compute Pmin for MDPs hannah 2021-05-21 01:34:23 +0200
  • fc0ae2ea4b removed SolveGoal in function computeLTLproabilities of SparseLTLHelper hannah 2021-05-20 23:41:11 +0200
  • 1fe30f7d78 Convert acceptance formula into disjunctive normal form hannah 2021-05-19 02:03:11 +0200
  • ffe70ea056 removed model from SparseLTLHelper hannah 2021-05-18 21:53:41 +0200
  • f8d9773131 test update hannah 2021-05-18 21:52:02 +0200
  • b30713c23d Started to restructure LTL model checking algorithms hannah 2021-05-15 22:42:31 +0200
  • 4fc3c79221 LTL tests for MDPs hannah 2021-04-27 10:10:39 +0200
  • 0f5c4708ca corrected exception hannah 2021-04-26 23:46:20 +0200
  • 884b284ab5 corrected exception hannah 2021-04-26 23:45:41 +0200
  • 466339059f Call parse_prefix_ltl instead of parse_formula hannah 2021-04-21 22:42:55 +0200
  • c290e16260 Simplified LTL2DeterministicAutomaton hannah 2021-04-21 21:29:59 +0200
  • d861c377a9 fixed typo hannah 2021-04-20 10:21:44 +0200
  • 6110d33bcc Removed debug output Tim Quatmann 2021-04-19 07:49:47 +0200
  • d44bc3c6c2 CMAKE: Added option to include and link against Spot Tim Quatmann 2021-04-16 15:37:38 +0200
  • d5edde05a7 Adapted ModelChecker test-cases and FormulaParser test-cases hannah 2021-04-15 10:10:31 +0200
  • 1c16c17a57 FragmentCheckerTest: Fixed a few more testcaes that now correspond to invalid formulae. Tim Quatmann 2021-04-14 16:26:55 +0200
  • b71cb813df FormulaParser: Fixed parsing of multi-bounded path operator and quantile operator Tim Quatmann 2021-04-14 15:31:57 +0200
  • 8c669b9e8b Fixed a FragmentCheckerTest case which considered a formula that is now considered invalid. Tim Quatmann 2021-04-14 15:30:30 +0200
  • aa29ad1196 flagging multi-objective and quantile formulae as StateFormulae (fixing the previous commit) Tim Quatmann 2021-04-14 15:29:49 +0200
  • cc9a4b8cb3 Adapting a parser test-case to the new parser Tim Quatmann 2021-04-14 12:20:15 +0200
  • 76c689a001 flagging multi-objective formulae as State formulae Tim Quatmann 2021-04-14 12:19:56 +0200
  • 4cf2fd7d61 Heavily refactored FormulaParser as it had become quite messy. Tim Quatmann 2021-04-13 15:56:32 +0200
  • 132c293105 TYPED_TESTS for LTL modelchecker hannah 2021-04-08 22:29:10 +0200
  • 7d74efd591 TYPED_TESTS for LTL modelchecker hannah 2021-04-08 22:26:37 +0200
  • 10e2d85cc4 Formulas: Added parentheses to formula output to avoid ambiguity Tim Quatmann 2021-04-08 16:50:12 +0200
  • bcf45f68df modelchecker test update hannah 2021-04-08 11:07:13 +0200
  • affee2bc5b ltl dtmc modelchecker tests hannah 2021-04-07 01:18:33 +0200
  • 02b77707d4 ltl dtmc modelchecker tests hannah 2021-04-07 00:46:03 +0200
  • b6800361ce ltl formula parser tests hannah 2021-04-07 00:45:00 +0200
  • 4fe4704f60 Silenced a couple of warnings triggered by cpphoafparser. Tim Quatmann 2021-03-11 10:27:04 +0100
  • 9ce6076689 Silenced a warning Tim Quatmann 2021-03-11 08:02:27 +0100
  • 3a769b3149 ToPrefixStringVisitor: Added missing case for GameFormula Tim Quatmann 2021-03-11 07:58:49 +0100
  • 819d97b712 (CTMC-LTL) FragmentSpecification: cslstar and csrlstar Joachim Klein 2020-08-24 22:25:19 +0200
  • 04a8bec83f (MDP-LTL) SparseMdpPrctlModelChecker: handle LTL Joachim Klein 2020-08-24 22:25:16 +0200
  • 615b2b5399 (MDP-LTL) SparseMdpPrctlHelper: computeSurelyAcceptingPmaxStates Joachim Klein 2020-08-24 22:25:15 +0200
  • 4c70f1a160 (MDP-LTL) ProductBuilder: DA product with MDP Joachim Klein 2020-08-24 22:25:15 +0200
  • c099183063 (MDP-LTL) MaximalEndComponent: containsAnyState Joachim Klein 2020-08-24 22:25:14 +0200
  • 5855a82e80 (MDP-LTL) CheckTask: negate() Joachim Klein 2020-08-24 22:25:13 +0200
  • b6b31f20af (MDP-LTL) AcceptanceCondition: extractFromDNF Joachim Klein 2020-08-24 22:25:13 +0200
  • cf6af6c456 (stateformula) Modelcheckers: support P[phi], Pmax/min[phi] where phi is a state formula Joachim Klein 2020-08-24 22:25:10 +0200
  • af10aa8b4b (stateformula) StateFormula: a StateFormula is a probabilistic path formula Joachim Klein 2020-08-24 22:25:09 +0200
  • a639836f6f (stateformula) CheckResults: provide constructor for quantitative from qualitative result Joachim Klein 2020-08-24 22:25:09 +0200
  • 27ca10a668 (stateformula) SymbolicQualitativeCheckResult: add getReachableStates() and getStates() accessors, like SymbolicQuantitativeCheckResult Joachim Klein 2020-08-24 22:25:08 +0200
  • 1243b9300c (LTL) SparseDtmcModelChecker: Implement LTL model checking Joachim Klein 2020-08-27 06:25:25 +0200
  • ab32af463b (LTL) AbstractModelChecker: detect need for LTL PMC, call (unimplemented) computeLTLProbabilities Joachim Klein 2020-08-24 22:25:05 +0200
  • 5427702376 WIP:needed? Boolean path formulas: allow storing context Joachim Klein 2020-08-24 22:25:05 +0200
  • fbe5236c4d (LTL) FragmentSpecification: add pctlstar() and prctlstar() fragments Joachim Klein 2020-08-24 22:25:04 +0200
  • 6404c526e2 WIP (LTL) LTL2DeterministicAutomaton (first hacky attempt) Joachim Klein 2020-08-24 22:25:01 +0200
  • 393dd2af87 (LTL) ExtractMaximalStateFormulasVisitor Joachim Klein 2020-08-24 22:25:03 +0200
  • b04d2723c2 (LTL) Add Formula::toPrefixString() Joachim Klein 2020-08-24 22:25:03 +0200
  • bd0a882cd5 (LTL) FormulaInformation: add containsComplexPathFormula() Joachim Klein 2020-08-24 22:25:01 +0200
  • 5482a32b8a (LTL) Refactor unary/boolean state formulas to allow path formulas as well Joachim Klein 2020-08-24 22:25:00 +0200
  • 256f9839da SparseDtmcPrctlModelChecker: computeDAProductProbabilities() Joachim Klein 2020-08-27 06:35:10 +0200
  • ad774e5138 WIP (HOA-path) FormulaParser: parse HOAPathFormula Joachim Klein 2020-08-24 22:24:56 +0200
  • ba907a1d75 WIP (HOA-path) FormulaParser: parse HOAPathFormula Joachim Klein 2020-08-24 22:24:56 +0200
  • aed8e53a29 (HOA-path) AbstractModelChecker: default handling for HOAPathFormulas (= reject) Joachim Klein 2020-08-24 22:24:56 +0200
  • 21b9d73816 WIP (HOA-path) logic: HOAPathFormula Joachim Klein 2020-08-24 22:24:55 +0200
  • 85a408dd72 (DA-product) tests: DAProductBuilderTest Joachim Klein 2020-08-24 22:24:59 +0200
  • 044074a4b1 (DA) tests: HOAParsingTest Stefan Pranger 2021-08-07 19:10:58 +0200
  • e5282708dd (DA-product) transformer: Product, DAProduct + builders Joachim Klein 2020-08-24 22:24:57 +0200
  • 3696e13736 (DA) ItemLabeling: addUniqueLabel, generateUniqueLabel Joachim Klein 2020-08-24 22:24:57 +0200
  • de0dd71679 (DA) Automata classes: DeterministicAutomaton, APSet, HOAConsumer, AcceptanceCondition Joachim Klein 2020-08-24 22:24:54 +0200