Public Member Functions | |
StateAbstraction (int numFields) | |
Create a new state abstraction relation for numFields abstraction class fields. | |
void | addField (int index, string abstracts, EqRel eq) |
Add new field to the end of the array. | |
void | resolve (IList implNames) |
Finishes adding fields and resolves implementation names to their index in implementation StateNodes. | |
bool | equal (StateNode abstr, StateNode impl) |
Return whether the two given StateNodes are equivalent. | |
override string | ToString () |
Private Attributes | |
string[] | abstracts |
Maps state array indices of the abstraction to the field name of the implementation. | |
EqRel[] | rel |
Maps state array indices of the abstraction to an EqRel. | |
int[] | abstractsIndex |
Maps state array indices of the abstraction to the respective state array index of the implementation. |
|
Create a new state abstraction relation for numFields abstraction class fields.
|
|
Add new field to the end of the array.
|
|
Return whether the two given StateNodes are equivalent. The state abstraction must be resolve()d for this.
|
|
Finishes adding fields and resolves implementation names to their index in implementation StateNodes. Resets abstracts to null.
|
|
|
|
Maps state array indices of the abstraction to the field name of the implementation.
|
|
Maps state array indices of the abstraction to the respective state array index of the implementation. Created by resolve() from abstracts. |
|
Maps state array indices of the abstraction to an EqRel.
|