7041 Commits (9d81730fe3f9801309060cff9065edf2ea18208d)
 

Author SHA1 Message Date
Matthias Volk 9d81730fe3 Fixed JSON import after changes in BEs 6 years ago
Matthias Volk 365b7e7673 Removed mChildren in DFTRestriction 6 years ago
Matthias Volk 723caeb56e Removed mChildren in DFTGate 6 years ago
Matthias Volk 56636fc4b0 Added missing break statement 6 years ago
Matthias Volk ed94c79c1a Continue refactoring 6 years ago
Matthias Volk 10c29d936b Refactoring DFT elements 6 years ago
Matthias Volk c91033ebb1 Fixed bitshift for DFT isomorphism 6 years ago
Matthias Volk 3bf14c5198 Larger refactoring for DFT BEs. Split into BEExponential and BEConst 6 years ago
Matthias Volk 3183a141d6 Started on support for constant failed/failsafe BEs 6 years ago
Matthias Volk 1f5d3b9479 Correct initialization of priority queue 6 years ago
Matthias Volk 19ba1c38e7 Set correct order for priorities according to heuristic 6 years ago
Matthias Volk ef16ba576c Added default case for switch 6 years ago
Matthias Volk 144fa1c898 Throw exception instead of assertion 6 years ago
Matthias Volk 6dbe2441b9 Removed unnecessary members 6 years ago
Matthias Volk 2ebac862e2 Added test cases for DFT approximation 6 years ago
Matthias Volk 7a8dbf8828 Heuristic is argument for functions in approximation algorithm 6 years ago
Matthias Volk 5d8fc7db77 Removed approximation heuristic NONE 6 years ago
Matthias Volk 37d0b66e73 Some fixes for approximation 6 years ago
Matthias Volk 6eb2795b68 Fixed crucial bug marking all states as 'to expand'. 6 years ago
Matthias Volk 0904c01828 Make exploration heuristic choosable 6 years ago
Matthias Volk e53d946b04 Refactored BucketPriorityQueue 6 years ago
Matthias Volk 6afcaa291d Refactored DftExplorationHeuristic 6 years ago
Matthias Volk 34edb426be Fixed arguments for exploration heuristic settings 6 years ago
TimQu eb15177801 cli: try to recover after checking a property has failed. (related to GitHub issue #42) 6 years ago
TimQu e8003769ca JaniParser: Better error messages for property parsing. 6 years ago
TimQu e2dc274977 Added export for globally properties in JANI. 6 years ago
TimQu e9119154d7 JaniParser: Fixed parsing of globally formulas in JANI. (GitHub issue #42) 6 years ago
TimQu a7a3a82d89 Prism: ToJaniConverters now enforces variables occurring in properties to become global. This fixes GitHub issue #40 6 years ago
TimQu 98e0fcd113 jani::Property: Flagged functions of PropertyInterval as const 6 years ago
TimQu 91b763d218 JaniExporter: Export accumulation for LRA properties correctly. 6 years ago
TimQu 0d8ecaff35 JaniParser: Transform reward bounds into time- or step bound if appropriate. Added some checks and warnings. 6 years ago
TimQu f2fe674656 JaniParser: made the model available when parsing the property. 6 years ago
TimQu 8313dc5ef1 Flipped the condition for an exception. 6 years ago
TimQu 3280cb867e Updated changelog. 6 years ago
TimQu c7aec92dc9 modelchecker: Added support for non-trivial reward accumulations for Sparse/Hybrid/Dd engines. 6 years ago
TimQu c43e13172f Jani: Accumulations for Smin/Smax properties. 6 years ago
TimQu bc3c0d1d55 ModelBase: added isDiscreteTimeModel(). and let isNondeterministicModel return true for POMDPs and PSGs. 6 years ago
TimQu 415e806531 RewardModelInformation: Fixed getting wrong reward informations in case of non-transient variables in reward expression. 6 years ago
TimQu fd2e4efc0b Fixed output of TotalRewardFormulae with non-trivial reward accumulation. 6 years ago
TimQu 33127c9b6e JaniNextStateGenerator: Fixed references to the unpreprocessed model. 6 years ago
TimQu d9d8b8db98 Silenced a confusing warning. 6 years ago
TimQu 176133f712 Respecting reward accumulations for long-run-average properties. 6 years ago
Tim Quatmann 5869a1f5fd Simplified StronglyConnectedComponentDecomposition. 6 years ago
Matthias Volk 8cbfd720f8 Set sysroot for cudd to fix issue with moved header files in macOS Mojave 6 years ago
Matthias Volk 22cbc9446f Added virtual destructors in cpptempl 6 years ago
Matthias Volk c0c242a191 Fixed compiler error under new Xcode 10.2 6 years ago
TimQu c37e2bfe70 Added INFO output when game solver is invoked. 6 years ago
TimQu dbc465b9de SCCDecomposition: Fixed topological sort of SCCs connected via '0'-valued transitions 6 years ago
TimQu 9dcbd69c09 CMake: Added a comment why we link statically against mathsat on macOS. 6 years ago
Tim Quatmann a2190c04b0 Added new versions to FindGurobi.cmake 6 years ago