search

cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

Detection of contradictory rules #196

Open ftc opened 7 years ago

ftc commented 7 years ago

The issue exists currently that rules which are non deterministic can be accidentally created. In general this problem seems hard to solve, however we can exploit the current structure of the rules to make a reasonable checker which may have a false positive.

Currently the format of my rules is

matcher |(+/-) effect

The matcher is a regular expression which ends in a positive callin or callback such as ...; [CI] foo() |- [CI] bar(). As long as we don't have two rules where the last literal of the matcher is the same and the effect is the same but with different enable/disable status there cannot be a contradictory rule.

This check may break down at some point in the future but it is a reasonable sanity check for now.

The following zip file contains a case where I accidentally wrote contradictory rules.

sim_issue.zip

ftc commented 7 years ago

This was my issue, I had a non deterministic enable/disable. I am closing it since its a duplicate of issue #147