6844 Commits (595afcfc0aa29a5dde8458f1a5c4d29913c8f1ca)
 

Author SHA1 Message Date
TimQu e2cb1dd78a fixed ToJaniConverter for the case where not all variables are global 6 years ago
TimQu bb04291860 fixed parsing of jani-function: two passes are required as functions can be defined before they are used 6 years ago
TimQu a95331948c fixed operator<< of function call expr 6 years ago
TimQu ee9e6354a3 removed standard-compliant option: storm-conv now produces standard compliant jani code by default 6 years ago
TimQu 13bc33328a fix in toJaniConverter 6 years ago
TimQu 646b668bd4 Added a new mdp model checker test 6 years ago
TimQu f50f1c2ee4 Fixed parsing of jani function definitions 6 years ago
TimQu ea1a1d97ef fixed export of jani functions to json. Remove output to cout when writing the jani file 6 years ago
TimQu c3837968dd nicer output for storm-conv and fixed an issue in storm-conv related to substituting constants before translating the functions 6 years ago
TimQu ccb5a89de3 Formula substitutions need to be performed before constant substitutions because otherwise, constants appearing in formula expressions can not be handled properly 6 years ago
TimQu 0e0f2c2390 fixed substitution of prism formulas 6 years ago
TimQu 5f9949bfbf reduce nesting for jani expressions 6 years ago
Matthias Volk 7f799ecb28 Fixed return of local variable 6 years ago
Matthias Volk 4ccc837434 Fixed setting correct model type for JaniGSPNBuilder 6 years ago
TimQu 90095a5455 correct conversion of prism formulas to jani functions when modules were renamed 6 years ago
TimQu 6e2046e357 fixed formula substitution within renamed modules of a prism program 6 years ago
TimQu c388d1c8fe making sure that functions in jani models and formulas in prism programs are substituted before flattening the model 6 years ago
TimQu 4d74ec501a substitute formulas in properties after parsing 6 years ago
TimQu 71489a24f5 The model builders now substitute jani functions (if still present) 6 years ago
TimQu 487f370c58 fixed getting the function identifier 6 years ago
TimQu a173cb68b8 fixed some janibuilder tests 6 years ago
TimQu aa6fd3cbb2 fixed compilation of storm-conv 6 years ago
TimQu 340c7f0db7 fixed getting the function identifier 6 years ago
TimQu 55efedb713 prism2jani no longer fails if a reward model has the same name as a formula/variable 6 years ago
dehnert 032d68b9b0 switching to recursive synchronization resolution for JANI explicit model exploration 6 years ago
TimQu 1b7f150e76 implemented functionality to rename reward model names 6 years ago
TimQu 2dd5c65051 fixed duplicated symbol linker error 6 years ago
TimQu 1190f32b56 cleanup in jani parser 6 years ago
dehnert 205ed7f4bf special treatment of trivial initial states restriction for JANI (following PRISM) next-state generator 6 years ago
TimQu f89817da3b eliminating reward accumulations directly at parsing time 6 years ago
TimQu 28d4dd481d simplified processing of janiConversionOptions 6 years ago
TimQu 101b49b898 detect unsupported jani-features directly upon parsing the model. 6 years ago
TimQu ae1987f64c Function and array eliminator now do not perform any action, if the corresponding model feature is not enabled 6 years ago
TimQu 4453eb4134 substitute jani-functions during preprocessing (analogous to prism program preprocessing) 6 years ago
TimQu e85b9759e2 better parsing of model features 6 years ago
TimQu ede671ea3f fixed wrong type mask for arrays... 6 years ago
TimQu 90c9e95c8a Only consider the reachable set of states after closing an MA 6 years ago
TimQu 034fbf20c7 extended SubsystemBuilder, made ChoiceSelector work for MAs as well. 6 years ago
TimQu bdeacf8669 better treatment of cases where array out of bounds accesses occurr 6 years ago
TimQu 7bae50d0ba fixed correct parsing of prism formulas 6 years ago
TimQu 10ae6a0dd8 fixed not respecting negative assignment indices in array eliminator 6 years ago
TimQu 8836e7a676 made pgcl2jani and gspn2jani compile again 6 years ago
dehnert 5e43c51f49 starting on some builder optimizations 6 years ago
TimQu 092a43a0a5 fixed correct export of modulo operator 6 years ago
TimQu d47189f93e fixes for array elimination 6 years ago
TimQu 5dda7a5296 removed unused file 'variable substitution visitor' 6 years ago
TimQu b5bb87404c replaced occurrences of 'substituteConstants' by 'substituteConstantsFormulas' 6 years ago
dehnert 7af70a77aa slight fix to bit vector sizes used in explicit model builder 6 years ago
TimQu c052da15b9 conversion from prism to jani respects formulaas 6 years ago
TimQu 3cf9553126 actually fixed model feature support 6 years ago