6471 Commits (13bc33328ae50770ddf934dff6d040f2eaf08483)
 

Author SHA1 Message Date
TimQu 7ee196bdbb jani2jani conversions in storm-conv 7 years ago
TimQu 7c61a16d91 fixes for array expressions, support to translate properties that consider array expressions, translating array models in cli 7 years ago
TimQu 274bfef652 started to extend storm-conv for array elimination 7 years ago
TimQu 69cbc28547 fixes for arrays 7 years ago
TimQu ba68562740 moved array variable replacement information into VariableInformation 7 years ago
TimQu ed45fa80e6 debugging array elimination 7 years ago
TimQu fdd3334e6f properly implemented model features 7 years ago
TimQu a7bb70f698 exporting array expressions 7 years ago
TimQu 6aaafea554 added possibility to lift transient edge destination assignments to the edge by scaling with the probability (only if this preserves the considered properties). 7 years ago
TimQu e2cb68b31f Enable array elimination in jit builder 7 years ago
TimQu c5a0a057c8 array elimination and assignment levels in janiNextStateGenerator 7 years ago
TimQu 4aff82c649 array eliminator replaces lvalues and variables 7 years ago
TimQu 32180591c0 extended jani datastructures 7 years ago
TimQu dadf571934 const and non-const jani traverser 7 years ago
TimQu 6564abd434 jani expression substitution now also works for array expressions 7 years ago
TimQu ea6b211703 fixed storing the wrong pointers to Variables in LValues 7 years ago
TimQu 5e01151617 jani-array fixes 7 years ago
TimQu dac431b263 parsing of jani-arrays 7 years ago
TimQu a9274d841c Merge branch 'master' into jani-arrays 7 years ago
TimQu 539b3230eb when exporting jani, eliminate reward accumulation kinds whenever they do not have any effect 7 years ago
TimQu 8050f8fc67 eliminate reward accumulations on jani level 7 years ago
TimQu 6cc0369a1c added JaniTraverser to conveniently traverse all components of a jani model. 7 years ago
TimQu 1714126a6f traverser for jani models 7 years ago
TimQu a739ce38f1 export of reward accumulations 7 years ago
TimQu 831f07e867 eliminate reward accumulations whenever possible 7 years ago
TimQu 701f3832b1 parsing reward accumulations 7 years ago
TimQu ee1dcbd483 fragment checker checks reward accumulations 7 years ago
TimQu 4302aa0be0 added missing include 7 years ago
TimQu 76b2eb2ee9 added reward accumulation to formulas 7 years ago
TimQu 234ddb7cff fixed compilation of JaniParser 7 years ago
TimQu a012539323 cleared some TODOs in the Jani Parser 7 years ago
TimQu 953d570ff0 fix in syntacticalEquality checker 7 years ago
Matthias Volk c136b9c628 Removed old jani file settings 7 years ago
TimQu ad88992ba2 export gspns to ctmcs/mdps if no intermediate/timed transitions occur. 7 years ago
TimQu 251c9e2141 added option to make the json export more compact 7 years ago
TimQu e038fb64be Jani: export the correct accumulation parameters for expected reward properties 7 years ago
TimQu 0f97eb89db binary storm-gspn now exits with 0 if no gspnfile is given 7 years ago
TimQu 4861b8d4b4 More robust parsing of capacities and allowing constants in GSPN properties 7 years ago
TimQu c124ebcc93 Fixed a Jani-related issue when adding assignments to OrderedAssignments 7 years ago
TimQu 5f201da6da correctly parse templates, weights, priorities 7 years ago
TimQu 1f40a56ed8 updated changelog 7 years ago
TimQu a44eed65e8 allowing constant definitions for gspns via cli 7 years ago
TimQu 3215af6fc0 Implemented single- infinite- and k- server semantics for timed gspn transitions 7 years ago
TimQu 49930ebc9e fixed help text 7 years ago
TimQu 7f601058a1 flatten option should not require module prefix 7 years ago
TimQu f9f6b90cc2 updated changelog 7 years ago
TimQu 4b3e7849ed jani parser parses array variables 7 years ago
TimQu 8202f77943 array expressions 7 years ago
TimQu 8da922e4d5 started to include array support 7 years ago
TimQu 5b78393425 Fixed issues related to allowing local variables when converting from prism to jani 7 years ago