Closed GoogleCodeExporter closed 9 years ago
Original comment by tonyohm...@gmail.com
on 21 Jan 2014 at 8:44
Solution in revision 2109:9e3f9572563e, please review
Original comment by sebastia...@gmail.com
on 6 Feb 2014 at 5:49
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
Original comment by bestchai
on 15 Jul 2014 at 7:08
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
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
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
Original issue reported on code.google.com by
bestchai
on 21 Jan 2014 at 3:02