search

Ecdar / j-Ecdar

A model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems) written in Java.
MIT License
4 stars 9 forks source link

Log actual state pair instead of location pair in refinement #82

Closed magoorden closed 1 year ago

magoorden commented 2 years ago

The refinement code has the following debug logging line:

Log.debug("Picked state pair " + locPair.leftLocation.getName()+"-"+locPair.rightLocation.getName());

So the line claims to print out the state pair, while it is actually printing out the location pair. It should print out the state pair, as the valuations of the variables are important for the forward reachability analysis performed by the refinement check.

magoorden commented 2 years ago

Solving this should help in investigating some of the test cases mentioned in #79.