Difference between revisions of "D45 Model Checking"
From Event-B
Jump to navigationJump to searchimported>Leuschel |
imported>Leuschel |
||
| Line 2: | Line 2: | ||
{{TODO}} An overview of the work done about model checking. | {{TODO}} An overview of the work done about model checking. | ||
| − | Driven by SSF usage of ProB: state compression: simplify states stored | + | 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 <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. | ||
| − | |||
= Motivations = | = Motivations = | ||
Revision as of 14:52, 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.
Motivations
TODO To be completed.
Choices / Decisions
TODO To be completed.
Available Documentation
TODO To be completed.
Status
TODO To be completed.
