A | |
| Abstraction [CfLazyModelChecker.Make_Lazy_Model_Checker] | |
| Ast |
This module defines the internal representation used
by BLAST to represent expressions and predicates.
|
C | |
| C_Command [Main] | |
| C_System_Descr [Main] | |
| CfLazyModelChecker |
This module implements the lazy model checking algorithm.
|
| Constant [Ast] | |
E | |
| Expression [Main] | |
| Expression [Ast] | |
I | |
| IntMap [CfLazyModelChecker.Make_Lazy_Model_Checker] | |
| IntSet [Main] | |
L | |
| LazyModelChecker |
This module implements the lazy model checking algorithm.
|
M | |
| Main | |
| Make_Lazy_Model_Checker [CfLazyModelChecker] | |
| Make_Lazy_Model_Checker [LazyModelChecker] | |
O | |
| Operation [CfLazyModelChecker.Make_Lazy_Model_Checker] | |
P | |
| Predicate [Main] | |
| Predicate [Ast] |
A predicate is a boolean combination of atomic expressions.
|
R | |
| Region [CfLazyModelChecker.Make_Lazy_Model_Checker] | |
S | |
| Stats [Main] | |
| Stats [CfLazyModelChecker] | |
| Symbol [Ast] | |
T | |
| Tree [CfLazyModelChecker.Make_Lazy_Model_Checker] |