35 Commits (990d1c97596abe98e2f0f6b7c4622c6fdd24799f)

Author SHA1 Message Date
Tim Quatmann dd7dc4b797 Towards allowing CLN numbers for RationalNumbers again. 5 years ago
Matthias Volk c039b817ef Removed unused variable + dependent code 5 years ago
Tim Quatmann c83721066c Use acyclic solver in reward bounded properties. 5 years ago
Matthias Volk 4ee31063a4 Removed double whitespaces in outputs 5 years ago
Tim Quatmann bc623d1203 MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler. 6 years ago
Tim Quatmann b4f652bbc8 Reducing the nesting when creating a expression::sum(...). 6 years ago
Tim Quatmann 1ae0200b51 Quantiles: fixed some bugs related to one or three dimensional quantile queries. 6 years ago
Tim Quatmann c40ecae2e6 Implemented quantiles for DTMCs. 6 years ago
Tim Quatmann aa3a1f5ff7 Quantiles: Improved performance by excluding already analyzed epochs from the created epochSequences 6 years ago
Tim Quatmann 971f4c8508 Quantiles: Fixed analysing epochs unnecessarily, fixed having multiple quantile formulas over the same variables. 6 years ago
Tim Quatmann c21ea2ce1f Quantiles: Bug fixes. 6 years ago
Tim Quatmann 8a72aee764 QuantileFormulas: ignore optimization direction (min/max) for quantile variables. 6 years ago
Tim Quatmann 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. 6 years ago
Tim Quatmann c33ac18a5a Quantiles: Fixed a precision related issue in new implementation. 6 years ago
Tim Quatmann 8ae9a6f5d6 quantiles: Further improved the implementation as in the paper 6 years ago
Tim Quatmann 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. 6 years ago
TimQu 88ee0bbf67 RewardUnfolding: If statistics are enabled, Log when an acyclic epoch model is found. 6 years ago
TimQu 5ad100e652 quantiles: Added some statistics. 6 years ago
TimQu fb7078770d rewardbounded: Various fixes. 6 years ago
TimQu dd93b1dae9 rewardbounded: Improved code structure. 6 years ago
TimQu 6aeb75e3bd quantiles: Supporting two-dimensional quantiles with the same optimization direction of quantile bounds (max,max or min,min). 6 years ago
TimQu a99dd5e4d1 quantiles: Better code re-usage, better structure, support for 'open' and 'non-open' dimensions, single dimensional quantiles should work now. 6 years ago
TimQu 1d5f2410b5 rewardBounded/RewardUnfolding: Allowed the case that not all dimensions have a bound a priori. 6 years ago
TimQu 4ac23d630f quantiles: Added support for formulas with trivial bounds (i.e., >=0). 6 years ago
Tim Quatmann 6e8aef2acc Checking formulas with >=0 bound. 6 years ago
Tim Quatmann f99a24acd2 more work on quantiles. 6 years ago
Tim Quatmann 82402ba3ae rewardbounded: Moved epoch model analysis to a separate file. 6 years ago
TimQu d796ee74de (workplace switch) 6 years ago
Tim Quatmann d3abeb5f45 Started implementation on quantiles. 6 years ago
TimQu dc2654ce60 Quantiles: made the SparseMdpPrctlModelChecker call the QuantileHelper for quantile formulas 6 years ago
TimQu c59d2160ee Implemented (multi-dimensional) cost bounded properties for DTMCs (sparse engine only) 7 years ago
TimQu 31ba64f018 bugfixes 7 years ago
TimQu ccf7521250 Multi-dimensional cumulative reward formulas 7 years ago
TimQu c9beea4f33 better lower/upper result bounds 7 years ago
TimQu 86253fe88a moved multidimensional unfolding implementation from multiobjective into helper namespace 7 years ago