You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I haven't looked into this in depth yet. But, as I mentioned to @barrucadu in person, the issue is most likely that an incorrect equation of bigger size was found then rewritten to an equation of smaller size. (The bigger the size of an equation, the larger the number of tests we need to falsify it). This causes the confusing behaviour of having an otherwise unfound equation of smaller size when size limit is increased.
To avoid this happening, before reporting equations, maybe Speculate should test them again with either the set number of tests or a separate larger number of tests. Perhaps also report a warning to the user that the number of tests should be increased as an incorrect equation was found.
@barrucadu reports an issue when applying Speculate to DejaFu:
speculate -t20000 -s5
: doesn't find any equalities, only conditional equations.speculate -t20000 -s6
: finds these equalities:(isBarrier a == synchronises a crid) == (False == isCommit a crid)
...
Property 1 is wrong. Something gets weird with ThreadActions ("ta") when the size is increased, even though the number of tests remains the same.
The text was updated successfully, but these errors were encountered: