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

Commit Graph

  • 98bb05b86f Trying to build spot with a single thread Tim Quatmann 2021-08-05 11:31:22 +0200
  • 3a3587370e Skip a test if LTL model checking is not available. Tim Quatmann 2021-08-05 11:30:41 +0200
  • efeeea0d54 Spot: re-iterated cmake interface to hopefully make it more clean. Added documentation on how to update spot Tim Quatmann 2021-08-04 16:33:07 +0200
  • e76c5ab4ba Fixed ambiguous operator overload. Tim Quatmann 2021-08-03 15:54:46 +0200
  • 5a2e489403 github buildtest workflow should test with spot. Tim Quatmann 2021-08-03 15:30:24 +0200
  • 4e6d334f9b Updated Changelog Tim Quatmann 2021-08-03 15:16:10 +0200
  • ba1d0d052d added simulator to tests Stefan Pranger 2021-08-08 12:15:06 +0200
  • 093b01f0c5 adjusted scheduler dontCare hannah 2021-08-03 13:51:41 +0200
  • adc5d9ae68 MA scheduler export hannah 2021-07-30 01:03:10 +0200
  • 1f17b31bbe arbitrary choice for dontCareStates hannah 2021-07-30 01:02:44 +0200
  • ebdfb2def8 keep the original modeltype during product construction hannah 2021-07-29 23:36:10 +0200
  • c80a62ce06 added function for computation of memory states hannah 2021-07-27 21:35:48 +0200
  • 71100e9d65 scheduler json export hannah 2021-07-27 20:42:38 +0200
  • cceb3513ce set states to dontCare during scheduler computations, adapted Tests hannah 2021-07-27 14:10:36 +0200
  • f92b2104b5 TODOs and fixed an error during scheduler creation hannah 2021-07-27 11:07:10 +0200
  • 6b0aaeadb4 ignore dontCare States while printing hannah 2021-07-27 11:05:41 +0200
  • 77ced0aefe fixed warning hannah 2021-07-21 23:59:55 +0200
  • c057e437e4 CMAKE: Do not mark STORM_USE_SPOT as advanced. Tim Quatmann 2021-07-21 12:36:51 +0200
  • 9626c3c5f1 Cmake: Fixed output when including spot. Tim Quatmann 2021-07-21 12:06:26 +0200
  • c1b06f40b7 CMAKE: Added option to include and link against Spot Tim Quatmann 2021-07-21 12:02:42 +0200
  • 412489a57f Added possibility to set (un)reachable states for scheduler hannah 2021-07-21 10:19:21 +0200
  • 214d586d10 fixed scheduler choice in EC hannah 2021-07-20 16:48:31 +0200
  • 6865ae1464 build memory structure from all states hannah 2021-07-20 16:31:49 +0200
  • 5c204182eb Added some todos Tim Quatmann 2021-07-20 14:16:16 +0200
  • b8712041bf fixed memory structure hannah 2021-07-16 16:41:42 +0200
  • 1191e3068f more ltl scheduler tests hannah 2021-07-16 16:40:41 +0200
  • 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