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

Commit Graph

  • 5f7bf64d44 Some refactoring Matthias Volk 2019-04-05 19:10:14 +0200
  • 99651bdc71 Started on the notion of 'relevant events' for DFT analysis Matthias Volk 2019-04-05 19:07:48 +0200
  • 3280cb867e Updated changelog. TimQu 2019-04-05 16:40:53 +0200
  • c7aec92dc9 modelchecker: Added support for non-trivial reward accumulations for Sparse/Hybrid/Dd engines. TimQu 2019-04-05 16:40:42 +0200
  • c43e13172f Jani: Accumulations for Smin/Smax properties. TimQu 2019-04-05 16:31:44 +0200
  • bc3c0d1d55 ModelBase: added isDiscreteTimeModel(). and let isNondeterministicModel return true for POMDPs and PSGs. TimQu 2019-04-05 16:31:04 +0200
  • 415e806531 RewardModelInformation: Fixed getting wrong reward informations in case of non-transient variables in reward expression. TimQu 2019-04-04 21:43:38 +0200
  • fd2e4efc0b Fixed output of TotalRewardFormulae with non-trivial reward accumulation. TimQu 2019-04-04 21:41:40 +0200
  • 33127c9b6e JaniNextStateGenerator: Fixed references to the unpreprocessed model. TimQu 2019-04-04 21:41:06 +0200
  • d9d8b8db98 Silenced a confusing warning. TimQu 2019-04-04 21:40:01 +0200
  • 176133f712 Respecting reward accumulations for long-run-average properties. TimQu 2019-04-04 21:39:34 +0200
  • 26366e43cf Some more refactoring Matthias Volk 2019-04-05 16:13:24 +0200
  • 694c87c2b1 Fixed JSON import after changes in BEs Matthias Volk 2019-04-04 17:23:09 +0200
  • 5ba2c6357e Removed mChildren in DFTRestriction Matthias Volk 2019-04-04 11:21:24 +0200
  • 20b123ceca Removed mChildren in DFTGate Matthias Volk 2019-04-04 11:04:40 +0200
  • 722ff138e2 Added missing break statement Matthias Volk 2019-04-04 00:31:43 +0200
  • 6787d01e29 Continue refactoring Matthias Volk 2019-04-04 00:31:29 +0200
  • ff22a973de Refactoring DFT elements Matthias Volk 2019-04-03 23:17:43 +0200
  • 1d7c5caaf2 Fixed bitshift for DFT isomorphism Matthias Volk 2019-04-03 17:26:32 +0200
  • 9dbb66a9bd Larger refactoring for DFT BEs. Split into BEExponential and BEConst Matthias Volk 2019-04-03 17:15:11 +0200
  • d3479071ac Set sysroot for cudd to fix issue with moved header files in macOS Mojave Matthias Volk 2019-03-27 10:09:37 +0100
  • 36601c8187 Added virtual destructors in cpptempl Matthias Volk 2019-03-27 10:08:59 +0100
  • c1798ded37 Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-04-02 10:37:34 +0200
  • 5869a1f5fd Simplified StronglyConnectedComponentDecomposition. Tim Quatmann 2019-03-28 18:06:33 +0100
  • 8cbfd720f8 Set sysroot for cudd to fix issue with moved header files in macOS Mojave Matthias Volk 2019-03-27 10:09:37 +0100
  • 22cbc9446f Added virtual destructors in cpptempl Matthias Volk 2019-03-27 10:08:59 +0100
  • fdf89e71a5 Started on support for constant failed/failsafe BEs Matthias Volk 2019-03-24 18:06:24 +0100
  • 87180e1000 Correct initialization of priority queue Matthias Volk 2019-03-24 18:05:21 +0100
  • f2e9d20a8d Set correct order for priorities according to heuristic Matthias Volk 2019-03-22 19:04:01 +0100
  • bd3e062988 Added default case for switch Matthias Volk 2019-03-22 18:58:34 +0100
  • 01461bbf57 Throw exception instead of assertion Matthias Volk 2019-03-22 10:15:37 +0100
  • 2c1855f69a Removed unnecessary members Matthias Volk 2019-03-19 16:23:52 +0100
  • 23233afe0b Added test cases for DFT approximation Matthias Volk 2019-03-19 14:46:25 +0100
  • a410b6d7bc Heuristic is argument for functions in approximation algorithm Matthias Volk 2019-03-19 14:45:30 +0100
  • 7b4a51effe Removed approximation heuristic NONE Matthias Volk 2019-03-19 11:28:14 +0100
  • 5d80c356e2 Some fixes for approximation Matthias Volk 2019-03-19 11:14:27 +0100
  • 42a79dfe88 Fixed crucial bug marking all states as 'to expand'. As a result no states were skipped during exploration and no approximation took place. Matthias Volk 2019-03-18 22:40:40 +0100
  • 970430a6fb Make exploration heuristic choosable Matthias Volk 2019-03-18 22:39:39 +0100
  • 3dd0bffef9 Refactored BucketPriorityQueue Matthias Volk 2019-03-18 22:02:36 +0100
  • bb5d8b478a Refactored DftExplorationHeuristic Matthias Volk 2019-03-18 22:01:07 +0100
  • b4bd898f1b Fixed arguments for exploration heuristic settings Matthias Volk 2019-03-13 14:15:59 +0100
  • c0c242a191 Fixed compiler error under new Xcode 10.2 Matthias Volk 2019-03-26 15:18:24 +0100
  • 289bfb7229 Added missing include. Tim Quatmann 2019-03-25 09:30:30 +0100
  • 889dc63059 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-03-25 09:21:34 +0100
  • c37e2bfe70 Added INFO output when game solver is invoked. TimQu 2019-03-25 09:10:13 +0100
  • dbc465b9de SCCDecomposition: Fixed topological sort of SCCs connected via '0'-valued transitions TimQu 2019-03-25 09:09:52 +0100
  • 9dcbd69c09 CMake: Added a comment why we link statically against mathsat on macOS. TimQu 2019-03-25 09:08:45 +0100
  • a2190c04b0 Added new versions to FindGurobi.cmake Tim Quatmann 2019-03-20 12:38:06 +0100
  • 1d52d577cb Fixed linking with Mathsat on macOS Tim Quatmann 2019-03-20 11:44:11 +0100
  • 90543ad499 Silenced a warning when building storm-pgcl Tim Quatmann 2019-03-20 11:43:28 +0100
  • 0920390430 Fixed permissive scheduler tests (GitHub issue #38). Tim Quatmann 2019-03-20 10:32:45 +0100
  • b9c38fe11a Fixed includes Matthias Volk 2019-03-20 11:42:30 +0100
  • 5d57746db2 If an option is unknown, Storm now prints a hint to similar option names. Tim Quatmann 2019-03-19 18:35:46 +0100
  • 19824976f7 Added helper script for downloading the QVBS Matthias Volk 2019-03-19 18:27:48 +0100
  • 01800f1590 Added string utility functions to find similar strings. Tim Quatmann 2019-03-19 16:04:46 +0100
  • 80bfa6b56e Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set. Tim Quatmann 2019-03-19 16:18:54 +0100
  • 27c2a8ba95 Added string utility functions to find similar strings. Tim Quatmann 2019-03-19 16:04:46 +0100
  • 5de1697edc Reading QVBS options from settings. Tim Quatmann 2019-03-19 16:00:42 +0100
  • 6b32bd1dc3 cmake: Added option to specify a path to the qvbs benchmarks. Tim Quatmann 2019-03-19 16:00:07 +0100
  • 6faf074fc5 Made sure that model::getAllParameters also returns the parameters occurring at rates. Tim Quatmann 2019-03-18 15:34:27 +0100
  • 12709f1625 Added parentheses to silence clang warning Matthias Volk 2019-03-19 10:14:07 +0100
  • be86014007 Added test for hecs-DFT Alexander Bork 2019-03-18 19:08:31 +0100
  • 98ce81e86a Jani: Fixed an issue where initial expressions for unbounded variables have not been substituted correctly. Tim Quatmann 2019-03-18 14:52:46 +0100
  • bc32853c28 Jani: Fixed an issue where initial expressions for unbounded variables have not been substituted correctly. Tim Quatmann 2019-03-18 14:51:10 +0100
  • 40f4141b56 Jani: Allowing bounded types for constants as pointed out in GitHub issue #37 Tim Quatmann 2019-03-18 14:13:25 +0100
  • c6fd015e6c Picking a default SmtSolver, even if no CoreSettings are available. Tim Quatmann 2019-03-18 14:09:37 +0100
  • ee6942c563 Merge branch 'quantiles_refactor' Tim Quatmann 2019-03-15 10:03:26 +0100
  • 84476b7000 Fixed getSmtSolver which previously did not respect the SmtSolver selection from the settings. Tim Quatmann 2019-03-15 10:03:19 +0100
  • d24f61ded6 Added tests for quantiles. Tim Quatmann 2019-03-15 10:01:29 +0100
  • 1ae0200b51 Quantiles: fixed some bugs related to one or three dimensional quantile queries. Tim Quatmann 2019-03-15 10:00:54 +0100
  • c40ecae2e6 Implemented quantiles for DTMCs. Tim Quatmann 2019-03-15 09:59:29 +0100
  • aa3a1f5ff7 Quantiles: Improved performance by excluding already analyzed epochs from the created epochSequences Tim Quatmann 2019-03-14 13:42:23 +0100
  • 971f4c8508 Quantiles: Fixed analysing epochs unnecessarily, fixed having multiple quantile formulas over the same variables. Tim Quatmann 2019-03-14 12:36:20 +0100
  • c21ea2ce1f Quantiles: Bug fixes. Tim Quatmann 2019-03-13 18:36:26 +0100
  • 8a72aee764 QuantileFormulas: ignore optimization direction (min/max) for quantile variables. Tim Quatmann 2019-03-13 18:04:16 +0100
  • 38121c28cb quantiles: permute point entries if the order of quantile variable definitions is not the same as the order of occurrence on a cost bound. Tim Quatmann 2019-03-13 18:02:13 +0100
  • e3fbb77362 JaniParser::parseFormula: Boolean connections of AtomicExpressionFormulas are now parsed as a single AtomicExpressionFormula (i.e. 'a>1 & b>2' becomes a single atomic proposition instead of having two propositions 'a>1' and 'b>2'). This reduces the number of labels that need to be considered and improves partial state space exploration for formulas such as 'P=? [F a>1 & b>2]'. TimQu 2019-03-13 12:03:06 +0100
  • 746c68d039 Merge branch 'master' into quantiles_refactor Tim Quatmann 2019-03-13 09:36:18 +0100
  • 004466b83f Fixed BitVector::full() for BitVectors with size 0 Tim Quatmann 2019-03-13 09:36:09 +0100
  • c33ac18a5a Quantiles: Fixed a precision related issue in new implementation. Tim Quatmann 2019-03-13 09:35:07 +0100
  • 8ae9a6f5d6 quantiles: Further improved the implementation as in the paper Tim Quatmann 2019-03-12 11:49:39 +0100
  • cde1c646d9 Started to implement the algorithm more close to the one mentioned in the paper (in particular to make things more clean and to allow more than 2 dimensions. Tim Quatmann 2019-03-11 19:09:05 +0100
  • 2ab7c34b4d Added tests for cycles and SEQ children Alexander Bork 2019-03-05 15:50:14 +0100
  • aa107dc88d Merge branch 'master' into dft Matthias Volk 2019-03-01 16:01:34 +0100
  • b4748064ac Warning about default dormancy factor of 1 as pointed out by Enno Ruijters Matthias Volk 2019-03-01 16:00:55 +0100
  • 15bcb8afb6 Output line number for GalileoParser errors Matthias Volk 2019-03-01 15:59:15 +0100
  • 0cc82e840a clean up Jip Spel 2019-03-01 11:00:49 +0100
  • a4e03ff941 Updated Changelog. We now have quantile queries. Tim Quatmann 2019-02-28 11:42:54 +0100
  • 5b8ad6fbbd Merge branch 'quantiles' Tim Quatmann 2019-02-28 11:39:11 +0100
  • f1abd89de1 Merge remote-tracking branch 'origin/master' into quantiles Tim Quatmann 2019-02-28 11:36:06 +0100
  • 0bf9f27e31 Fixed typo and renamed a variable. TimQu 2019-02-28 11:33:25 +0100
  • e89cbf2886 fixed cyclic check. TimQu 2019-02-27 00:55:46 +0100
  • d31fae859f Added error handling of gates with restricton as child and changed order of topoSort and rank computation to ensure that rank is only computed for acyclic DFTs Alexander Bork 2019-02-26 21:26:04 +0100
  • 88ee0bbf67 RewardUnfolding: If statistics are enabled, Log when an acyclic epoch model is found. TimQu 2019-02-26 15:11:25 +0100
  • 04082fb2d6 Added a method to check whether a graph contains a cycle. TimQu 2019-02-26 15:10:25 +0100
  • 3c5f25fe4a Get all model parameters Matthias Volk 2019-02-15 16:57:23 +0100
  • d7a22e78d0 Allow unnecessary parameters in region string Matthias Volk 2019-02-15 16:56:49 +0100
  • 6c543df537 Fix in bisimulation of MDPs, which failed if all non-absorbing states in the quotient are initial Sebastian Junges 2019-02-15 13:50:47 +0100
  • 6c2262b7e8 more informative error messages during model building (for better debugging) Sebastian Junges 2019-02-15 13:48:13 +0100
  • b59cbfa1de graph conditions for rewards described by rational functions with nonconstant denominators Sebastian Junges 2019-02-14 23:24:11 +0100