Formal verification directly on AUT graphs
Reachability graphs can be generated in AUT format. It would be interesting to verify properties directly on AUT graphs.
In that case, we could work on string labels like:
- label1 --> label2
- A[] label1 or label2
where the labels are defined in the AUT file.
Practically, the verification mechanism is easier since it consists of one or multiple graph visits that check the reachability of labels and loops. The usage of SafetyProperty, the evaluation mechanism of a property, and the fetching part of the algorithm in AvatarModelChecker could be partially reused.