search

chubbymaggie / synoptic

Automatically exported from code.google.com/p/synoptic
0 stars 0 forks source link

Use multiple event transitions for constrained refinement #332

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
During constrained model checking and refinement, we find the event transition 
with the min or max time delta (for lower and upper bound invariants, 
respectively).  During constrained refinement, we currently use this single 
transition with the min or max time delta to decide if there is a stitching at 
the current partition.

However, there may be multiple event transitions that are tied for the min or 
max time delta.  In this case, we need to make sure we have access to all of 
these so that during refinement, we can declare that there is a stitching only 
if *none* of these min/max transitions create a contiguous, non-stitched path.

Original issue reported on code.google.com by tonyohm...@gmail.com on 7 Aug 2013 at 4:19

GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
Correction: "... we can declare ..." in the last sentence above is incorrect.

Instead, we should consider all events which are targets of (min/max timed) 
event transitions into this partition from the previous partition in the path 
(set X).  We should also consider all events which are sources of (min/max 
timed) event transitions out of this partition into the next partition in the 
path (set Y).  If X != Y, there's a potential for a stitching.

More informally, the (min/max timed) event transitions we used to reach this 
partition must all be followed by (min/max timed) event transitions to the next 
partition in the path.  All of the former must connect to one of the latter, 
and all of the latter must come from one of the former, i.e., X==Y.

Original comment by tonyohm...@gmail.com on 12 Aug 2013 at 8:25

GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
Sorry for all the incorrect "solution" comments... This is for real.

Solution in revision 704d2733e2fc, please review.

Original comment by tonyohm...@gmail.com on 12 Aug 2013 at 10:20

GoogleCodeExporter commented 9 years ago 
Correct if I'm wrong, but I believe this is blocking on our discussion of the 
constrained refinement algorithm. I'll wait to review this until we've looked 
through the step-wise description of the algorithm and have come to a consensus 
of how it should behave (+ if this issue needs further work/changes).

Original comment by bestchai on 14 Aug 2013 at 4:23

GoogleCodeExporter commented 9 years ago 
That's right. This is on hold for now.

Original comment by tonyohm...@gmail.com on 14 Aug 2013 at 6:19

GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
Solution in revision 382c3b6004a0, please review.

Original comment by tonyohm...@gmail.com on 28 Aug 2013 at 6:14

GoogleCodeExporter commented 9 years ago 
Merged into default via Issue335 merge with revision dcba6587c52d

Original comment by tonyohm...@gmail.com on 1 Oct 2013 at 3:44