Dat3M
Dat3M copied to clipboard
Relation Model Implementation
This PR is related to #732 and contains the following:
- Implementation of
RelationModel, a representation of relations inDartagnandedicated for better witness generation, and the corresponding "RelationModelManager" that is responsible for construction ofRelationModeland computation of derived relations. - Support of witness generation for showing relations defined in the model
vmm.cat. Users may pass--witness.relationsToShow=r1,r2,r3...into the command to have witness for corresponding relations. - Add
LocalandAssertevents to witness graph. But note code of this part is temporary and needs to be refined, which will be done in the next step: implementation ofEventModel...