ticktac-project/tchecker

Improve covreach graph construction

Closed this issue · 1 comments

Current construction expands nodes by first adding all its child nodes and corresponding edges, and second removing those which are covered. This is done to ensure that edges are built correctly, in particular when a node is covered by one of its successors.

After a discussion with Philipp Schlehuber, it seems that we can cover nodes before we add them to the graph. We shall only take care of the situation where a node n is covered by one of its successors n1. Then, for all the following successors n2 we shall avoid adding the edge n->n2. This can be detected since n is inactive once it has been removed.

Solved in v0.3 (with a different solution)