Commit Graph

  • e59918668e
    AbstractEquationSolver: Added more convenient getters for the most appropriate lower/upper bound of a given variable Tim Quatmann 2021-03-10 06:26:59 +0100
  • 59c5aeadea changed message for boundedGloballyFormula Lukas Posch 2021-03-09 18:32:23 +0100
  • f6829dd109 clean up BoundedGloballyGameViHelper Lukas Posch 2021-03-09 18:14:49 +0100
  • 0fd952c6f7 removed b Lukas Posch 2021-03-09 18:00:20 +0100
  • bcd67c63f7 removed "...Reachability" from GameViHelper and BoundedGloballyGameViHelper Lukas Posch 2021-03-09 17:41:19 +0100
  • 5e040553a6 changed error message Lukas Posch 2021-03-09 17:32:01 +0100
  • 0ea549864f fixed assert for using lowerBounds Lukas Posch 2021-03-09 17:29:10 +0100
  • 02bc7f3f69 added assert for using lowerBounds Lukas Posch 2021-03-09 16:39:30 +0100
  • 6df0efcd3e
    Set result correctly for reachability rewards in MdpInstantiationChecker Matthias Volk 2021-03-09 13:03:17 +0100
  • 64861445fe bug fix bounded globally Lukas Posch 2021-03-09 12:59:47 +0100
  • eaff65ef27 LinearCoefficientVisitor: Fixed translation of division expressions. Tim Quatmann 2021-03-09 07:15:22 +0100
  • 5d45514af2 avoid parsing jani after creating model - fix in lvalue to allow this Sebastian Junges 2021-03-08 21:21:14 -0800
  • 3355b21b72 add timing info to storm-pomdp Sebastian Junges 2021-03-08 16:28:17 -0800
  • d6ab421cb7 add belief-support-mdp generator Sebastian Junges 2021-03-08 16:27:28 -0800
  • 3c58b5b2f7 case split for MDPs actually checks for MDPs Sebastian Junges 2021-03-08 16:19:18 -0800
  • 08f928456c fix guard for code that considers transient assignments to also consider only transient assignments Sebastian Junges 2021-03-08 16:18:24 -0800
  • 6b6f44100e allow building parametric models of the form s --p-->, s--q--> Sebastian Junges 2021-03-08 16:16:39 -0800
  • 8df4a99770 small changes, but did not fix the bug Lukas Posch 2021-03-08 17:54:46 +0100
  • 489d8a5fd2 added bounds to model checker and parse it for probability calculation of bounded globally formulas Lukas Posch 2021-03-08 12:42:23 +0100
  • 50c7a69f94 added bounds to computeBoundedGlobally Probabilities and parse upperBound to the game vi helper, additional little changes Lukas Posch 2021-03-08 12:41:14 +0100
  • 66f893edcb changed globally formula grammar and added the case for bounded globally formulas for createGloballyFormula Lukas Posch 2021-03-08 12:39:27 +0100
  • 023e067c59 added bounded globally formulas to other classes Lukas Posch 2021-03-08 12:37:50 +0100
  • e1599efc6f added upperBound to valueIteration of BoundedGloballyGameViHelper Lukas Posch 2021-03-08 12:34:19 +0100
  • ef415d4347 added needed methods to class BoundedGloballyFormula Lukas Posch 2021-03-08 12:33:20 +0100
  • dbc0cacb45 added bounded globally to AbstractModelChecker Lukas Posch 2021-03-08 12:31:20 +0100
  • 7beb999219 label unlabelled commands Sebastian Junges 2021-03-07 23:03:29 -0800
  • 71f60e812c more precise analysis of whether commands will synchronize Sebastian Junges 2021-03-07 23:02:57 -0800
  • c4187b03eb fixed error messages Sebastian Junges 2021-03-07 22:58:47 -0800
  • a5842e4a61 nasty bug where some sync action indices where not reflected in one of the data structures Sebastian Junges 2021-03-06 11:22:04 -0800
  • 7daa5e2ab7 fixed error message Sebastian Junges 2021-03-06 11:20:59 -0800
  • 52f88bca4d Merge branch 'master' into prismlang-sim Sebastian Junges 2021-03-05 22:50:45 -0800
  • 9fea07542a
    Fixed warning Matthias Volk 2021-03-05 11:52:02 +0100
  • c9841b71a0
    Const reference for splittingThreshold Matthias Volk 2021-03-05 11:51:14 +0100
  • 78b0bc9749 Merge branch 'main' into next_formulae Lukas Posch 2021-03-04 15:40:17 +0000
  • 5ace260ecb set up SparseSmgRpatlModelChecker for bounded globally Lukas Posch 2021-03-04 16:15:28 +0100
  • 4aee59a15a set up SparseSmgRpatlHelper for bounded globally Lukas Posch 2021-03-04 16:15:04 +0100
  • ff8c520808 added class BoundedGloballyGameViHelper Lukas Posch 2021-03-04 16:14:28 +0100
  • 9976b927f9 small changes and added TODOs in class BoundedGloballyFormula Lukas Posch 2021-03-04 16:14:01 +0100
  • 1fb1368a14 Set up BoundedGloballyFormula to methods of FragmentChecker.* Lukas Posch 2021-03-04 16:13:22 +0100
  • 5030efd363 Set up BoundedGloballyFormula to methods of FormulaInformationVisitor.* Lukas Posch 2021-03-04 16:13:09 +0100
  • c142922182 Set up BoundedGloballyFormula to methods of Formula.* Lukas Posch 2021-03-04 16:12:48 +0100
  • c1ab2ca8d9 created class BoundedGloballyFormula Lukas Posch 2021-03-04 14:31:30 +0100
  • 56e70c3417 setBoundedGloballyFormulasAllowed in FragmentSpecification.* Lukas Posch 2021-03-04 13:57:18 +0100
  • 8d17a0362d Fix extremal value computation Jip Spel 2021-03-04 11:41:57 +0100
  • 49dff36512
    Github Actions: clone complete history to support version extraction Matthias Volk 2021-03-03 22:51:43 +0100
  • 3437d76a55 Merge pull request 'next formulae' (#18) from next_formulae into main Stefan Pranger 2021-03-03 17:30:01 +0000
  • a86426211c changed statesOfCoalition Lukas Posch 2021-03-03 17:52:33 +0100
  • 2f39eab91e reduced the calculation part to a call to multiplyAndReduce in SparseSmgRpatlHelper.cpp Lukas Posch 2021-03-02 15:41:41 +0100
  • 5738701a2d removed scheduler handling from next (except a warning) Lukas Posch 2021-03-02 14:49:48 +0100
  • 2e27e32622 start with next formulae Lukas Posch 2021-03-01 19:13:45 +0100
  • 4514ed76d6 Merge branch 'master' into prismlang-sim Sebastian Junges 2021-03-02 21:45:55 -0800
  • d25cd1d636
    Enable Github Actions for pull requests (without deployment) Matthias Volk 2021-03-02 11:43:49 +0100
  • 2a86bfa14c Merge pull request 'globally formulae' (#17) from globally_formulae into main Stefan Pranger 2021-03-02 08:30:01 +0000
  • 60ce89872c fixed another small typo Lukas Posch 2021-03-01 19:15:33 +0100
  • 50087994f7 fixed typo Lukas Posch 2021-03-01 18:12:07 +0100
  • 3f9616d3e0
    Added documentation about integrating Github pull requests Matthias Volk 2021-03-01 18:10:26 +0100
  • 5b9319ee58 clean up computeGloballyProbabilities Lukas Posch 2021-03-01 18:00:57 +0100
  • 0ed64b6257 Add == and != ops to RelevantEvents Daniel Basgöze 2021-02-25 15:33:09 +0100
  • 7a2b060afc Remove allowDCForRelevant from RelevantEvents Daniel Basgöze 2021-02-25 15:27:24 +0100
  • 972ef8b14c Break inclusion loop in DFT.h Daniel Basgöze 2021-02-25 15:08:14 +0100
  • 7fc4046fbc
    Fix DftSimulatorTest for older Boost versions Matthias Volk 2021-02-23 19:36:13 +0100
  • 734599c114 correction of globally functionality Lukas Posch 2021-02-22 12:11:21 +0100
  • 76afd5e3de
    Implemented basis for handling invalid traces during simulation Matthias Volk 2021-02-08 20:37:41 +0100
  • 6eec25de6c
    Typos Matthias Volk 2021-02-08 20:35:04 +0100
  • 7111674ec8
    Support for simulation of PDEP Matthias Volk 2021-02-08 12:31:56 +0100
  • 9e3e2c02fe
    Handle PDEP in createSuccessorState as well Matthias Volk 2021-02-08 12:28:20 +0100
  • 6c025f13d2
    Added more tests for DFT simulation Matthias Volk 2021-01-25 20:55:57 +0100
  • 344ba353e0
    Use template for DFTTraceSimulator Matthias Volk 2021-01-25 20:50:48 +0100
  • fb2f55d804
    Fixed bug where POR was changed to PAND during transformation to binary FDEPs Matthias Volk 2021-01-25 20:14:42 +0100
  • d74558e0cb changelog update Sebastian Junges 2021-02-20 00:29:33 -0800
  • 42ec9ec60d state lookup does not crash when state does not exist Sebastian Junges 2021-02-20 00:28:30 -0800
  • c1fbe3c194 Merge branch 'master' into prismlang-sim Sebastian Junges 2021-02-19 23:56:05 -0800
  • bfd03bc9ce Merge branch 'rubicon' into prismlang-sim Sebastian Junges 2021-02-19 21:15:44 -0800
  • c1ec3032fa reset to state Sebastian Junges 2021-02-18 23:21:54 -0800
  • fded9732d2 Updated CHANGELOG Matthias Volk 2021-02-18 16:00:47 +0100
  • fcc1762595 Github actions: run doxygen daily instead of on push to prevent race condition Matthias Volk 2021-02-18 15:01:09 +0100
  • 08ea706cb4 Merge branch 'master' of origin Matthias Volk 2021-02-18 14:58:58 +0100
  • e7ca4dc0c9 start with globally formulae - definitions of methods and functionality (not checked) Lukas Posch 2021-02-17 22:31:39 +0100
  • 6d24ea9606 Silenced many 'loop variable is always a copy' warnings Tim Quatmann 2021-02-17 21:30:54 +0100
  • 481d23b904 Replaced storm::expressions::Expression::operator^ by storm::expressions::pow. An optional flag indicates if we should allow power expressions of integer type (PRISM semantics) or whether it is always a real (JANI semantics). Tim Quatmann 2021-02-17 20:56:08 +0100
  • 46462d6556 Z3Adapter: Fixing translation of XOR operators - expression's operator^ is supposed to be power, not xor. Tim Quatmann 2021-02-17 20:55:04 +0100
  • d863fe4156 Jani Export: Power expressions of integer type need to be type casted. Tim Quatmann 2021-02-17 19:54:44 +0100
  • 0d54b80ba5 Merge pull request 'until formulae' (#14) from until_formulae into main Stefan Pranger 2021-02-17 16:11:00 +0000
  • 94cd2e7fbd Apply rewriting only for modularisation Matthias Volk 2021-02-17 12:52:02 +0100
  • afa0c07947 introduced schedulerSize, removed empty for-loop Lukas Posch 2021-02-17 11:24:48 +0100
  • aa2489cb36 added some comments to expansion of scheduler Stefan Pranger 2021-02-16 17:29:20 +0100
  • e48f3d0705 added notPhiStates to expandScheduler Lukas Posch 2021-02-16 16:09:46 +0100
  • 646181c533
    Merge pull request #103 from ArashPartow/master Tim Quatmann 2021-02-16 15:10:00 +0100
  • f39538763f Reverted Fix for CUDD (fixes #104) Tim Quatmann 2021-02-16 14:14:28 +0100
  • 7807c8a143 changed variable names to camelCase Lukas Posch 2021-02-15 20:16:06 +0100
  • 5473966cd1 changed clippedStatesOfCoalition with size and values from relevantStates Lukas Posch 2021-02-15 20:04:14 +0100
  • 5dfe48e51e changed description of submatrix Lukas Posch 2021-02-15 19:18:52 +0100
  • e1cbf08749 Removed DEBUG messages, changed description of submatrix Lukas Posch 2021-02-15 19:06:35 +0100
  • 86bf1a0d89 small clean up Lukas Posch 2021-02-15 16:51:08 +0100
  • 318544a940 refactor computation of relevantStates from BitVector method to logical AND Lukas Posch 2021-02-15 16:45:14 +0100
  • 7a25fb7881 small code clean up, added todo for refactoring bitvector method Lukas Posch 2021-02-15 16:03:34 +0100
  • 37d36c52b3 fill up the result vector for ~relevantStates Lukas Posch 2021-02-15 15:46:07 +0100
  • 58ec5b89e9 set direction overrides Lukas Posch 2021-02-15 14:55:04 +0100
  • 781f105ca1 introduced name relevantStates, moved methods to Bitvector class Lukas Posch 2021-02-11 17:42:39 +0100
  • 2bf6402725 implemented until formulae Lukas Posch 2021-02-09 22:14:47 +0100