Difference between revisions of "D45 Model Checking"
imported>Leuschel |
imported>Leuschel |
||
| Line 5: | Line 5: | ||
If the preference <tt>COMPRESSION</tt> is set to true, then ProB will also detect common (sub-)expressions and store them only once. | If the preference <tt>COMPRESSION</tt> is set to true, then ProB will also detect common (sub-)expressions and store them only once. | ||
E.g., when several states have the same same value for a given variable <tt>x</tt> then its value will only be stored once. | E.g., when several states have the same same value for a given variable <tt>x</tt> then its value will only be stored once. | ||
| + | |||
| + | Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing. | ||
| + | We have also implemented a SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB. | ||
| + | |||
= Motivations = | = Motivations = | ||
| Line 12: | Line 16: | ||
= Available Documentation = | = Available Documentation = | ||
{{TODO}} To be completed. | {{TODO}} To be completed. | ||
| + | |||
| + | * [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB Command-Line Version of ProB] | ||
| + | |||
= Status = | = Status = | ||
{{TODO}} To be completed. | {{TODO}} To be completed. | ||
[[Category:D45 Deliverable]] | [[Category:D45 Deliverable]] | ||
Revision as of 15:07, 10 February 2012
Overview
TODO An overview of the work done about model checking.
Driven by SSF usage of ProB: state compression: simplify states stored so that they require less memory. This was achieved without compromising speed. If the preference COMPRESSION is set to true, then ProB will also detect common (sub-)expressions and store them only once. E.g., when several states have the same same value for a given variable x then its value will only be stored once.
Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing. We have also implemented a SHA1 hashing function for Prolog terms, but it is not yet used in the production version of ProB.
Motivations
TODO To be completed.
Choices / Decisions
TODO To be completed.
Available Documentation
TODO To be completed.
Status
TODO To be completed.
