Bug in Issue351 IntrBy code

GoogleCodeExporter commented 9 years ago

Using the Issue351 branch and running this command:
$ ./synoptic.sh -c traces/abstract/osx-login-example/args.txt
traces/abstract/osx-login-example/trace.txt

The output looks like:

Exception in thread "main" Internal error, notify developers.
Error: Could not satisfy invariants: [login attempt IntrBy(t) auth
failed, auth failed IntrBy(t) login attempt]
Error traceback:
Internal error, notify developers.
Error: Could not satisfy invariants: [login attempt IntrBy(t) auth
failed, auth failed IntrBy(t) login attempt]

Error traceback:
at 
synoptic.algorithms.Bisimulation.splitUntilAllInvsSatisfied(Bisimulation.java:13
9)
at synoptic.main.SynopticMain.runSynoptic(SynopticMain.java:830)
at synoptic.main.SynopticMain.main(SynopticMain.java:122)
at 
synoptic.algorithms.Bisimulation.splitUntilAllInvsSatisfied(Bisimulation.java:13
9)
at synoptic.main.SynopticMain.runSynoptic(SynopticMain.java:830)
at synoptic.main.SynopticMain.main(SynopticMain.java:122)

This comes up when Synoptic cannot satisfy the invariant because the
partitions are refined to contain one event instance (for the invalid
path).

It looks like a problem with the miner, as login attempt IntrBy(t) auth failed 
and auth failed IntrBy(t) login attempt are both mined, and that should never 
be possible.

Original issue reported on code.google.com by bestchai on 21 Jan 2014 at 3:02

GoogleCodeExporter commented 9 years ago

Original comment by tonyohm...@gmail.com on 21 Jan 2014 at 8:44

GoogleCodeExporter commented 9 years ago

Solution in revision 2109:9e3f9572563e, please review

Original comment by sebastia...@gmail.com on 6 Feb 2014 at 5:49

Changed state: Started

GoogleCodeExporter commented 9 years ago

Just to explain, so that you do not have to look into all the commit messages:
It is of course possible to mine the two invariants, I added test cases that 
should document this Issue. Also, the definition of the IntrBy invariant 
explains it. The problem was a wrong implementation of the unconstrained INtrBy 
FSM (Tracing Set), which resulted in too many counterexamples.

Original comment by sebastia...@gmail.com on 6 Feb 2014 at 6:47

GoogleCodeExporter commented 9 years ago

Original comment by bestchai on 15 Jul 2014 at 7:08

Changed state: Fixed

GoogleCodeExporter commented 9 years ago

I am new to synoptic and I am interested in using it. I am having the same 
problem but with my own dataset. I am wondering if it is because a bug, or 
problem with the dataset.

Exception in thread "main" Internal error, notify developers.
Error: Could not satisfy invariants: 
[routing-key=conductor,method=object_class_action,args:{objmethod=get_by_virtual
_interface_id,objname=FixedIPList} IntrBy(t) 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_network_
and_host,objname=FixedIP}, 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_virtual_
interface_id,objname=FixedIPList} IntrBy(t) 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_uuid,obj
name=Network}]
Error traceback:
Internal error, notify developers.
Error: Could not satisfy invariants: 
[routing-key=conductor,method=object_class_action,args:{objmethod=get_by_virtual
_interface_id,objname=FixedIPList} IntrBy(t) 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_network_
and_host,objname=FixedIP}, 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_virtual_
interface_id,objname=FixedIPList} IntrBy(t) 
routing-key=conductor,method=object_class_action,args:{objmethod=get_by_uuid,obj
name=Network}]
Error traceback:

    at synoptic.algorithms.Bisimulation.splitUntilAllInvsSatisfied(Bisimulation.java:137)
    at synoptic.main.AbstractMain.runSynoptic(AbstractMain.java:797)
    at synoptic.main.SynopticMain.main(SynopticMain.java:49)

    at synoptic.algorithms.Bisimulation.splitUntilAllInvsSatisfied(Bisimulation.java:137)
    at synoptic.main.AbstractMain.runSynoptic(AbstractMain.java:797)
    at synoptic.main.SynopticMain.main(SynopticMain.java:49)

Original comment by swk.e...@gmail.com on 11 Aug 2014 at 9:20

GoogleCodeExporter commented 9 years ago

Just to provide some extra information, exceptions happen only for some random 
seeds. I can get the results for at least 1 run.

Original comment by swk.e...@gmail.com on 11 Aug 2014 at 9:29

GoogleCodeExporter commented 9 years ago

Hello swk.easy,

One major issue here is that Synoptic should not be using the IntrBy(t) 
invariant type (this type should only be available in Perfume). I changed the 
code to make sure that Synoptic doesn't use this invariant type.

Can you check out the latest code from the default branch (revision 
3b3b6fd8c65f) and see if this fixes it for you?

best,
ivan.

Original comment by bestchai on 12 Aug 2014 at 2:36

oryanfuchs / synoptic

Bug in Issue351 IntrBy code #352