You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Tree: f13ca25f6c

accumulation

accumulation-v4.7

automata-finite

master

tud-infrastructure-2018-10-12

Branches Tags

${ item.name }

Create tag ${ searchTerm }

Create branch ${ searchTerm }

from 'f13ca25f6c'

${ noResults }

prism-accumulation/prism/src/hybrid

History

Dave Parker e8bb5b2880 Store and report on accuracy information for numerical model checking queries. Accuracy info for numerical results is computed and stored during model checking. For now, it is always the worst-case accuracy over all states for which results are computed. The information is stored in a class prism.Accuracy, instances of which are created in a consistent fashion using prism.AccuracyFactory. Accuracy info is stored in the prism.Result class. Accuracy information is generated for all 4 main engines (sparse/hybrid/MTBDD/explicit), and attached to the Result object when model checking the filter that is wrapped around a property (currently, just for the default "state" filter). The accuracy is printed with the main result at the end of model checking. e.g.: Result: 0.1666666865348816 (+/- 1.1920928955078125E-7; rel err 7.152556520395694E-7) For now, accuracy info is generated for the majority of properties for DTMCs and MDPs (no support yet for multi-objective model checking). For methods like value iteration, where a guaranteed error bound is not generated, convergence information is used, but reported as being only an estimate. Test mode has been updated (code in prism.ResultTesting) to use the reported accuracy of a result to check correctness against a reference result. If it is missing, or only estimated, the old approach of using default check of 1e-5 with relative error is used. For the explicit engine, accuracy info is stored in explicit.ModelCheckerResult, returned by most numerical computation methods i.e. those in the explicit.ModelChecker and explicit.IterationMethod (sub)classes. At a higher level, the accuracy info is then stored in explicit.StateValues, when this created from ModelCheckerResult in explicit.ProbModelChecker. For symbolic (sparse/hybrid/MTBDD) engines, the error bound info from C++ code is stored in a variable last_error_bound that be accessed (or reset) from prism.PrismNative, using the methods getLastErrorBound() and resetModelCheckingInfo(). At a higher level, this is then stored in subclasses of prism.StateValues, which are created in the prism.*ModelChecker classes from the results of computations.		6 years ago
..
Makefile	Makefile: replace hardcoded directory names with PRISM_*_DIR	7 years ago
PH_JOR.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_JORInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_NondetBoundedUntil.cc	PH,PM,PS: cast jints to int in printf	9 years ago
PH_NondetReachReward.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_NondetReachRewardInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_NondetUntil.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_NondetUntilInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_PSOR.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_PSORInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_Power.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_PowerInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_ProbBoundedUntil.cc	PH,PM,PS: cast jints to int in printf	9 years ago
PH_ProbCumulReward.cc	PH,PM,PS: cast jints to int in printf	9 years ago
PH_ProbInstReward.cc	PH,PM,PS: cast jints to int in printf	9 years ago
PH_ProbReachReward.cc	fix compilation issue: cmath / isinf	9 years ago
PH_ProbReachRewardInterval.cc	fix compilation issue: cmath / isinf	9 years ago
PH_ProbTransient.cc	PH,PM,PS: cast jints to int in printf	9 years ago
PH_ProbUntil.cc	fix compilation issue: cmath / isinf	9 years ago
PH_ProbUntilInterval.cc	fix compilation issue: cmath / isinf	9 years ago
PH_SOR.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_SORInterval.cc	Store and report on accuracy information for numerical model checking queries.	5 years ago
PH_StochBoundedUntil.cc	sparse/hybrid stochastic: fix delete call in error case	8 years ago
PH_StochCumulReward.cc	symbolic stochastic computations: fix memory leak of the FoxGlynnWeights weights array	8 years ago
PH_StochSteadyState.cc	fix compilation issue: cmath / isinf	9 years ago
PH_StochTransient.cc	symbolic stochastic computations: fix memory leak of the FoxGlynnWeights weights array	8 years ago
PrismHybrid.cc	(native) switch includes from .h to C++ header wrappers	9 years ago
PrismHybrid.java	Store and report on accuracy information for numerical model checking queries.	5 years ago
hybrid.cc	hybrid.cc: initialise col_offset in hdd_negative_row_sums	8 years ago
package-info.java	Improved documentation (JavaDoc mostly).	15 years ago