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

Commit Graph

  • f28e59ab8d Polished SMG model Tim Quatmann 2021-01-13 12:11:14 +0100
  • 109a885c65 PlayerCoalition: Added a getter for players Tim Quatmann 2021-01-13 12:10:53 +0100
  • 4affb76bb1 Renamed Coalition to more descriptive PlayerCoalition Tim Quatmann 2021-01-13 10:57:46 +0100
  • 735874462c Polished fragment specification and formula visitors for new GameFormulas Tim Quatmann 2021-01-13 10:43:01 +0100
  • 4c5bc4e2a2 Polished GameFormula and Coalition code Tim Quatmann 2021-01-13 10:42:11 +0100
  • 2cf73f9b10 ModelType: Fixed capitalization of SMG output Tim Quatmann 2021-01-13 09:35:09 +0100
  • 4d4cd6e7f4 rpatl extends prctl Stefan Pranger 2020-12-16 11:04:55 +0100
  • 8e55ec62ad gameForumlas now gather referenced variables Stefan Pranger 2020-12-16 10:41:15 +0100
  • 6c97e9dc29 rpatl smg formulas now accept operatorFormulas Stefan Pranger 2020-11-24 16:05:13 +0100
  • 8d47ad2bd7 refactor Coalition to use boost variant Stefan Pranger 2020-11-23 18:09:24 +0100
  • 2972f43def removed print from CloneVisitor Stefan Pranger 2020-11-23 17:49:12 +0100
  • 3f2aaf72b0 fixed typo in arg list of GameFormula Stefan Pranger 2020-11-23 13:45:16 +0100
  • 2721f24b9b added Coalition default ctor Stefan Pranger 2020-11-23 13:44:46 +0100
  • 487eb13a24 WIP added grammar rules for gameFormula Stefan Pranger 2020-11-19 18:23:32 +0100
  • df52e5af88 added casting getter for gameFormula Stefan Pranger 2020-11-19 18:26:42 +0100
  • 2f5a53196c added rPATL to FragmentSpecifitcations Stefan Pranger 2020-11-19 18:11:20 +0100
  • 7d87a90c1e added multiple Visitor methods for gameFormulas Stefan Pranger 2020-11-19 18:08:51 +0100
  • 09cb1d465c added GameFormula class Stefan Pranger 2020-11-19 18:12:54 +0100
  • 310c9d21d4 added Coalition class Stefan Pranger 2020-11-19 18:13:20 +0100
  • bc5eec34d2 switch cases in engine now feature SMG case Stefan Pranger 2020-11-23 14:24:48 +0100
  • 875410a59e Polished ExplicitModelBuilder: * ChoiceInformationBuilder renamed to StateAndChoiceInformationBuilder, now also keeping track of state-based information (StateValuations, MarkovianStates, statePlayerIndications) * ModelComponents now consider statePlayerIndications and PlayerNamesToIndices separately Tim Quatmann 2021-01-13 08:58:40 +0100
  • 277f802850 * PlayerIndex is now declared in a separate file (as this can potentially be independent of PRISM input). * Polished PrismNextStateGenerator, in particular more proper error handling Tim Quatmann 2021-01-12 13:36:50 +0100
  • 3ba9ae637c
         Run doxygen deploy on push and do not keep history Matthias Volk 2021-01-12 12:36:17 +0100
  • d2c6420356 Add doxygen deploy workflow Daniel Basgöze 2020-12-17 20:41:04 +0100
  • df721f55d7 Cleanup comments Daniel Basgöze 2020-12-17 20:40:44 +0100
  • 97b2d751e0 * prism::Player's no longer keep track of module and action indices to reduce redundancies. * PrismProgram::CheckValidity and PrismProgram::simplify now treat SMGs properly * PrismProgram is now responsible for moduleIndex->playerIndex and actionIndex->playerIndex assignment * More defined behavior for actions that don't have a player (work in progress) Tim Quatmann 2021-01-12 11:00:05 +0100
  • 6fe76a009d Polished parsing of Prism-SMGs, in particular * Fixed issues related to module renaming that resulted from setting the module indices already in the first run * Fixed a few uint_fast32_t vs uint_fast64_t issues, created alias PlayerIndex Tim Quatmann 2021-01-12 07:09:18 +0100
  • 81db530f70 do not clear moduleToIndexMap for second run Stefan Pranger 2020-08-13 11:42:46 +0200
  • 52e30059e3 fix reorder warning Stefan Pranger 2020-11-23 14:25:35 +0100
  • e529045a8f Merge commit '6a71c19d8a5808b3a0c5be21f0966e8ada7f4252' into smg-merge Tim Quatmann 2021-01-11 14:32:58 +0100
  • 4a7ea35959 first version for action mask callbacks in explicit generator Sebastian Junges 2020-12-28 22:43:54 -0800
  • 7a38f54d01 extend the next state generator to support prism program simulation Sebastian Junges 2020-12-27 20:56:55 -0800
  • e5ed114715 a first simulator of prism files Sebastian Junges 2020-12-23 22:38:28 -0800
  • aa6a3d2142 sampling from a distribution and from a choice Sebastian Junges 2020-12-23 22:37:16 -0800
  • 00a85cb184 accessors for model Sebastian Junges 2020-12-23 22:36:47 -0800
  • b3f5cd1c89 fixed call of inherited function and Stefan Pranger 2020-12-23 11:02:42 +0100
  • 0e79f71435 change optimization direction if overridden Stefan Pranger 2020-12-22 17:38:56 +0100
  • 50fdc36387 check convergence with weighted values Stefan Pranger 2020-12-22 17:11:34 +0100
  • 505c830d42 set optdir overrides from multiplier env Stefan Pranger 2020-12-22 17:05:05 +0100
  • c7d7be8b83 nondetTs may also be gameNondetTs in LraViHelper Stefan Pranger 2020-12-22 17:02:21 +0100
  • de385b0527 added method for lra game transition type Stefan Pranger 2020-12-22 16:57:42 +0100
  • 4c7968b4cf added and finalized NondetGamehelper methods Stefan Pranger 2020-12-22 16:41:47 +0100
  • ea90c1ac7d added and finalized methods for rpatlMC Stefan Pranger 2020-12-22 16:30:40 +0100
  • f72f83f23e computeLongRunAverageValues is now virtual Stefan Pranger 2020-12-22 16:34:00 +0100
  • b61d947057 parse coalition operator and set row group optdirs Stefan Pranger 2020-12-22 16:10:05 +0100
  • 9ef1ec5f50 added opt dir override bitvector to multiplier Stefan Pranger 2020-12-22 16:07:02 +0100
  • c11c49d22b store tuples of player name and index Stefan Pranger 2020-12-22 15:58:30 +0100
  • e610edc197
         Run github actions daily Matthias Volk 2020-12-17 21:44:50 +0100
  • 741d04c797 Implement manually triggered github actions CI Daniel Basgöze 2020-12-15 19:53:59 +0100
  • af38bc3b4d added transition type for games to LraViHelper Stefan Pranger 2020-12-16 12:45:36 +0100
  • 02695da9b7 Fixed several issues regarding powers with negative exponents. Tim Quatmann 2020-12-16 12:33:36 +0100
  • a3ada8a0c3 cli: added a space that was missing in output of steady-state result Tim Quatmann 2020-12-16 12:32:53 +0100
  • 0a689d232e init helper for games Stefan Pranger 2020-12-16 12:15:16 +0100
  • 19839036af AbstractMC passes game formula to the rpatl MC Stefan Pranger 2020-12-16 11:47:01 +0100
  • 0a65e4aa7b verification now handles SMGs Stefan Pranger 2020-12-16 11:42:54 +0100
  • 21af5c5d6a handle model description ostream case for SMGs Stefan Pranger 2020-12-16 11:36:41 +0100
  • b599ff5c7e added sparse MC templates for SMGs Stefan Pranger 2020-12-16 11:35:50 +0100
  • d1a0299bd0 buildMatrices handles playerIndices via reference Stefan Pranger 2020-12-16 11:33:47 +0100
  • e88a83d9aa engine now checks smg models Stefan Pranger 2020-12-16 11:27:48 +0100
  • a299504361 added smg rpatl model checker Stefan Pranger 2020-12-16 11:25:05 +0100
  • d939ebe375 smg model now stores the player action indices Stefan Pranger 2020-12-16 11:19:45 +0100
  • 353b98ec88 rpatl extends prctl Stefan Pranger 2020-12-16 11:04:55 +0100
  • 1470d65586 gameForumlas now gather referenced variables Stefan Pranger 2020-12-16 10:41:15 +0100
  • 4dcd1cfb64 Fixed simplification of expressions that use the power operator with negative exponents. Tim Quatmann 2020-12-15 11:32:02 +0100
  • 09cb0e5a5d LraCtmcTest: Renamed a testcase as its name was misleading before. Tim Quatmann 2020-12-14 11:57:07 +0100
  • 5245d77bfc SteadyState: Issue a warning in sound mode because it is not supported. Tim Quatmann 2020-12-14 11:56:21 +0100
  • 818f8cb8ee steadystate: Added a testcase. Tim Quatmann 2020-12-14 11:55:42 +0100
  • b73e2e5d1c Fixing steady state distribution computation. Tim Quatmann 2020-12-11 18:48:23 +0100
  • 77d2e9c98f Fixed output of steady-state distr computation. Tim Quatmann 2020-12-11 18:25:19 +0100
  • 211a72b6d7 fixing compilation of storm-pars Tim Quatmann 2020-12-11 17:36:43 +0100
  • 19e6473806 making the cudd warning sound a bit less dangerous Tim Quatmann 2020-12-11 17:21:04 +0100
  • 2e593dc014 Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Tim Quatmann 2020-12-11 17:08:55 +0100
  • 28ab011eb8 Added an export of check results to json. Tim Quatmann 2020-12-11 16:29:01 +0100
  • 84e6984659 StateValuations::toJson now has a template parameter to change the exported type of rationals. Tim Quatmann 2020-12-11 15:53:55 +0100
  • 75b6ac27e8 JaniParser: Making result field optional (fixes #83) Tim Quatmann 2020-12-01 14:59:26 +0100
  • 3184ba1611 Jani: Correctly parse the input-enable field. Throw an error in the sparse model builder, as these are not supported right now. Tim Quatmann 2020-12-01 14:51:55 +0100
  • 41ae9d5624 Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20) Tim Quatmann 2020-11-30 11:48:35 +0100
  • 6cea196953 rpatl smg formulas now accept operatorFormulas Stefan Pranger 2020-11-24 16:05:13 +0100
  • 51f86db9eb Storm version 1.6.3 Tim Quatmann 2020-11-24 12:48:07 +0100
  • 7002946845 Updated changelog. Tim Quatmann 2020-11-24 10:10:55 +0100
  • 251527bccf storm-pars: Make a more explicit warning if a non-parametric equation solver type is selected. Tim Quatmann 2020-11-24 10:09:09 +0100
  • 1243feba8c Substitute constants in JANI Properties (fixes #95) Tim Quatmann 2020-11-23 22:01:38 +0100
  • a9868fd501 refactor Coalition to use boost variant Stefan Pranger 2020-11-23 18:09:24 +0100
  • 84bcfef24e removed print from CloneVisitor Stefan Pranger 2020-11-23 17:49:12 +0100
  • 2fb1f36fda Merge branch 'keep-module-index-map-in-parsing' into game_formula_parsing Stefan Pranger 2020-11-23 17:17:28 +0100
  • 53ac9a3873 fixed typo in arg list of GameFormula Stefan Pranger 2020-11-23 13:45:16 +0100
  • 376e4756db added Coalition default ctor Stefan Pranger 2020-11-23 13:44:46 +0100
  • 73e4945818 add STORM_DEVELOPER ALL_WARNINGS GCC case Stefan Pranger 2020-11-23 13:20:46 +0100
  • f106b83328 WIP added grammar rules for gameFormula Stefan Pranger 2020-11-19 18:23:32 +0100
  • 715784a070 added casting getter for gameFormula Stefan Pranger 2020-11-19 18:26:42 +0100
  • 8dc46968cb added rPATL to FragmentSpecifitcations Stefan Pranger 2020-11-19 18:11:20 +0100
  • c52fcba6a2 added multiple Visitor methods for gameFormulas Stefan Pranger 2020-11-19 18:08:51 +0100
  • 6dd9e09ede added GameFormula class Stefan Pranger 2020-11-19 18:12:54 +0100
  • cbbafaddfd added Coalition class Stefan Pranger 2020-11-19 18:13:20 +0100
  • 2225ebcbe8 fix reorder warning Stefan Pranger 2020-11-23 14:25:35 +0100
  • eba20bb005 switch cases in engine now feature SMG case Stefan Pranger 2020-11-23 14:24:48 +0100
  • 065b366198 Removed superfluous '.' in output of Markov automata model data. Tim Quatmann 2020-11-23 10:37:51 +0100
  • 6d6e142236 Fixed an issue with JANI models concerning properties using transient variable expressions. Tim Quatmann 2020-11-20 12:25:29 +0100
  • ee5fff680a Indefinite Horizon helpers: Do not compute values of MaybeStates if they are not relevant for the property. (Fixes #87) Tim Quatmann 2020-11-20 10:35:02 +0100
  • 20d424e289 JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists. Tim Quatmann 2020-11-20 09:36:59 +0100