prism-accumulation

4052 Commits

5 Branches

0 Tags

31 MiB

Branch: accumulation-v4.7

Commit Graph

Author	SHA1	Message	Date
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
Joachim Klein	4de3c189a4	Build: Switch from javah (deprecated since JDK8) based JNI header generation to javac As noted in #68, the javah tool has been removed in JDK10. Here, we switch to the new way of generating the JNI .h files, using the -h option of the regular javac compiler. We have to adapt all Makefiles (not only those in directories that contain classes with native methods), as javac compiles all required classes (and generates their JNI headers) beyond the directory with the Makefile. The .h files generated by javac -h had a different naming scheme, now there is a prefix for the package name. To avoid having to touch all the #includes, we generate the new .h files in prism/include/jni and provide legacy headers in the old location and with the old name, forwarding the the corresponding new header. In the future, at an appropriate moment, those legacy headers can be removed and replace with direct includes. Currently, there is a post-processing step on Windows: After the .h file is generated, dos2unix is called to replace the Windows CRLF line endings. Otherwise, the generated headers show up as changed files in version control. As now there are no special targets for the generation of the .h files anymore, we move to a global post-processing step and call dos2unix on prism/include/jni/*.h at the end of building.	8 years ago

Author

SHA1

Message

Date

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

Joachim Klein

4de3c189a4

Build: Switch from javah (deprecated since JDK8) based JNI header generation to javac

As noted in #68, the javah tool has been removed in JDK10. Here, we switch to the new way of generating the JNI .h files, using the -h option of the regular javac compiler.

We have to adapt all Makefiles (not only those in directories that contain classes with native methods), as javac compiles all required classes (and generates their JNI headers) beyond the directory with the Makefile.

The .h files generated by javac -h had a different naming scheme, now there is a prefix for the package name. To avoid having to touch all the #includes, we generate the new .h files in prism/include/jni and provide legacy headers in the old location and with the old name, forwarding the the corresponding new header. In the future, at an appropriate moment, those legacy headers can be removed and replace with direct includes.

Currently, there is a post-processing step on Windows: After the .h file is generated, dos2unix is called to replace the Windows CRLF line endings. Otherwise, the generated headers show up as changed files in version control. As now there are no special targets for the generation of the .h files anymore, we move to a global post-processing step and call dos2unix on prism/include/jni/*.h at the end of building.

8 years ago

2 Commits (accumulation-v4.7)