Feature #42

[Experiment] Ignore abstract node regions in Cegar's trace checking

Added by Grégoire Sutre almost 6 years ago. Updated over 5 years ago.

Status:Closed Start date:09/16/2011
Priority:High Due date:10/09/2011
Assignee:Grégoire Sutre % Done:

100%

Category:-
Target version:1.2

Description

Every abstract counterexample corresponds to a path in the model's automaton. This path might be feasible even though the abstract counterexample is spurious. Moreover, if the path is not feasible, the trace-checking engine may provide a better path invariant when abstract nodes are ignored.

To test this idea, modify Cegar's trace_of_fwd_path and trace_of_bwd_path functions so that they simply use Region.top in place of abstract node regions.

This is just an idea to experiment.


Related issues

precedes McScM - Feature #20: Lazy Cegar Tree Closed 10/10/2011

History

Updated by Grégoire Sutre over 5 years ago

In McMillan's Lazy Abstraction with Interpolants paper, the regions labeling nodes of the abstract reachability tree are discarded for refinement. Indeed, the path interpolant is generated from the sequence of transition formulas, and the latter only depend on the program's instructions.

So it might be interesting to experiment with the passing/discarding of abstract regions for the LazyAbstraction module as well.

A uniform solution would be to have a functor that takes a trace-checking engine and returns a new trace-checking engine where the passed state regions are replaced by the top region. The resulting trace invariant must then be reduced to conform with the specification of trace checkers.

Updated by Grégoire Sutre over 5 years ago

  • Assignee set to Grégoire Sutre
  • Priority changed from Normal to High
  • Target version set to 1.2
  • Start date set to 09/16/2011
  • % Done changed from 0 to 50

Irreducibility of trace invariants turns out to be important for the in-progress Lazy Abstraction engine. To conform with McMillan's paper, it is desirable to drop regions labeling nodes, but the resulting trace invariant is not irreducible anymore.

Hence, we give this issue higher priority. The implementation should provide a functor taking as input a trace-checking engine and returning a trace-checking engine where state regions are replaced by top in the input trace. To avoid useless reductions, it will probably be necessary to tag trace-invariants with a boolean telling whether they are (known to be) irreducible or not.

Updated by Grégoire Sutre over 5 years ago

  • Status changed from New to In Progress

Updated by Grégoire Sutre over 5 years ago

  • Due date set to 10/09/2011
  • Status changed from In Progress to Closed
  • % Done changed from 50 to 100

The functor TraceCheckerUtil.DiscardStates has been added in commit 1170.

On second thought, it did not seem crucial to add irreducibility information in the trace invariants. So we keep the property that trace-checking engines shall always return irreducible invariants.

Also available in: Atom PDF