Use time constraints during model checking

[GoogleCodeExporter]

synoptic.invariants.fsmcheck.TracingStateSet children should be added for each 
constrained invariant (AFby upper, AFby lower, AP upper, and AP lower).  This 
will also require some modifications to FsmModelChecker because transition 
times will need to be passed to the constrained TracingStateSet classes.

Original issue reported on code.google.com by tonyohm...@gmail.com on 14 Jun 2013 at 2:43

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

Original comment by tonyohm...@gmail.com on 14 Jun 2013 at 2:46

[GoogleCodeExporter]

Original comment by tonyohm...@gmail.com on 14 Jun 2013 at 2:56

• Changed state: Started

[GoogleCodeExporter]

A few minor code review notes for revision ced02cfe2e6d:

- The FsmModelChecker.getCounterExample() returns null iff the model satisfies 
an invariant. For the un-implemented constrained invariant types you should 
throw an exception (e.g., the NotImplementedException) instead of returning 
null. This is neater and hass less potential for confusion.

- Always use braces to surround if/else branches. One negative example of this 
that I saw is in APUpperTracingSet.transition where you check for 
!tCurrent.lessThan(t). It looks a rare occurrence, but good to be vigilant. 

- The @SuppressWarnings("unchecked") annotation on APUpperTracingSet.transition 
hides three warnings, all of which have to do with 
TracingStateSet.preferShorter. I think you should (1) resolve these by making 
preferShorter static, and parameterizing it with something that extends 
HistoryNode, and (2) try to use the annotation sparingly. It's okay if the 
warnings are visible -- they reveal code inadequacies and let us know what to 
work on!

Original comment by bestchai on 11 Jul 2013 at 9:24

[GoogleCodeExporter]

1. I recognize what I've done is bad practice, but it's the only way I can get 
synoptic to run while I've only got 1 of the 4 tracing state sets implemented.  
Development would be much harder without being able to actually run the system, 
so this is a temporary bad practice that I'll fix when APUpper is working (and 
I then quickly implement the other 3).

2. Oops. Fixed.

3. Fixed.

Original comment by tonyohm...@gmail.com on 19 Jul 2013 at 7:06

[GoogleCodeExporter]

Solution in revision 9258540dc66e, please review

Original comment by tonyohm...@gmail.com on 6 Aug 2013 at 10:40

[GoogleCodeExporter]

Here are some code review notes:

- Add a top-level comment for ConstrainedTracingSet class to describe the 
purpose of the class and how it fits into the architecture of the project.

- I'm getting an assertion error when running APUpperCounterExamplePathTest. 
The triggered assert is in

ConstrainedTracingSet.toCounterexample:
  // TODO: why do we require isTerminal here?
  assert (cur.node).isTerminal();

First, you should make sure you can reproduce this. If you can't perhaps you 
need to somehow enable assertions in Eclipse prefs?

Second, I think this TODO and assert are not necessary. As we discussed, it's 
okay for the counter-example path to be incomplete, so both statements are okay 
to remove.

- I would refactor ConstrainedTracingSetTests.getPartitions() into two loops, 
both of which iterate through graph.getNodes(). The first will find the 
getFirst and the second will find the getSecond. The current code has too much 
nesting to be easy to read.

Also, this getPartitions seems to only work on the simple graph. I would add a 
comment to make this explicit -- if the graph is more complex, then this method 
can return unexpected results.

- Bisimulation.getSplitsConstrained() is getting long and difficult to read 
(and it's not even complete yet!). My recommendation is to factor out the loop 
that starts with:
            for (EventNode curEv : curPart.getEventNodes()) {
into a separate function. It would also make it easier to test :-)

I would also implement the splitting on curPart logic (tbd at the bottom of 
getSplitsConstrained) in a separate function, as well.

(It's unfortunate that these key methods in Bisimulation are static. This makes 
it a pain to track and pass around state. Auto-method-refactoring in Eclipse is 
your friend here. But, we might want to consider making the Bisimulation class 
instances more stateful.)

- ConstrainedTracingSet has a few cryptic variables that need to be renamed:
List<ConstrainedHistoryNode> s;
List<ITime> t;

- I'm a bit confused about your usage of ConstrainedTracingSet.s. It looks like 
you are using it in APUpperTracingSet to store states of the constrained FSM. 
And, you plan to re-use it by having more/fewer elements in this list, for 
other tracing sets. Is this right?

If so, this is nicely extensible, but it does complicate readability. I wish 
each of those s[0], ... , s[3] was actually a variable in APUpperTracingSet, 
with a readable name that had some easy-to-understand meaning. This is what 
APTracingSet does -- it has firsA, firstB, neitherSeen as the equivalents of 
s[0], s[1], s[2]. I think you're better off removing the s and implementing the 
more semantically-friendly version.

(And, if you really want a general means of handling all of these states across 
invariants, then you can always build the list of these states dynamically.)

- In the ConstrainedTracingSet.getMinMaxTime method, the long if condition that 
starts with:
  if (minMaxTime == null...

Needs parenthesis. I'm pretty sure that without parens the logic is broken 
there. Also, this is a good reminder to write simpler code. There's no reason 
not to have two separate functions -- one for min and one for max. Yes, it adds 
a method, but the complexity of both methods will be low in comparison with the 
current method.

Also, this getMinMaxTime (regardless of whether or not you refactor it into two 
methods) does not belong in ConstrainedTracingSet. You want this in ITime ... 
except that ITime is an interface, so we need a bit of refactoring to create an 
abstract class that implements ITime that is then inherited by the other, 
existing, time classes. The getMinMaxTime method should be a static method in 
this non-existing class. This task is nicely scoped for a new issue.

Original comment by bestchai on 8 Aug 2013 at 1:12

[GoogleCodeExporter]

- Add a top-level comment for ConstrainedTracingSet
  == Done

- I'm getting an assertion error ... make sure you can reproduce this ... I 
think this TODO and assert are not necessary
  == Done, and I agree (this was a carry-over from unconstrained model checking). Removed.

- I would refactor ConstrainedTracingSetTests.getPartitions() into two loops 
... seems to only work on the simple graph. I would add a comment
  == Done, and done (I hadn't thought of that).

- Bisimulation.getSplitsConstrained() is getting long ... My recommendation is 
to factor out ...
  == Because this is exactly what Issue 331 is about, is it okay if I do this in that branch instead?

(It's unfortunate that these key methods in Bisimulation are static. ... 
Auto-method-refactoring in Eclipse is your friend here. But, we might want to 
consider making the Bisimulation class instances more stateful.)
  == Which specific refactoring do you mean?  And making it more stateful could be part of Issue 331, since that would make it more testable as well.

- ConstrainedTracingSet has a few cryptic variables that need to be renamed
  == Done

- ... ConstrainedTracingSet.s. It looks like you are using it in 
APUpperTracingSet to store states of the constrained FSM. ... Is this right?
  == Yes

... it does complicate readability. I wish each of those s[0], ... , s[3] was 
actually a variable in APUpperTracingSet, with a readable name that had some 
easy-to-understand meaning. This is what APTracingSet does -- it has firsA, 
firstB, neitherSeen as the equivalents of s[0], s[1], s[2]. I think you're 
better off removing the s and implementing the more semantically-friendly 
version.
  == The problem is that not all states in constrained FSMs can have reasonable names.  APUpper is the easiest FSM, so we could have neitherSeen, firstASeen, firstAThenSomethingLegalSeen, and illegalBSeen.  Not as nice as unconstrained FSMs but not horrible.  The other constrained FSMs get worse though...  My solution was to document the states more thoroughly in javadocs, but if you still think giving them labels (or moving my explanations to elsewhere in javadoc) would be better, I can do that.

- In the ConstrainedTracingSet.getMinMaxTime method, the long if condition ... 
Needs parenthesis. ... have two separate functions -- one for min and one for 
max.
  == It actually is correct due to order of operations, but you're right that it's complex.  I've already changed this function to deal with transitions rather than times in the Issue 330 branch.  If I split it into two functions, there would be some code duplication (why I originally did it this way), so let me first try to make the logic very verbose in my next Issue 330 commit.  Let me know if you then still think I should split it, and I can do that.

... getMinMaxTime ... You want this in ITime ...
  == This is probably no longer relevant because of the Issue 330 changes mentioned above.

( Fixed in revision becb86513ba4 )

Original comment by tonyohm...@gmail.com on 8 Aug 2013 at 9:55

[GoogleCodeExporter]

Ok, I agree with all of your comments. Here are a few more things:

- I'm okay with keeping the ConstrainedTracingSet.states if we can't come up 
with easy-to-understand names for the individual states. You may want to add a 
note about this near where states are defined -- i.e., add the design rationale 
for choosing an anonymous list of states instead of naming them individually. I 
would also change the comment at top of APUpperTracingSet slightly to reflect 
the reference to the states list more directly, (e.g., States0 -> states.get(0) 
: Neither A nor B..).

- revision becb86513ba4 seems to have many of your fixes, but revision 
03bc3739a4f6 that merged in becb seems to be missing some of these (e.g., the 
class-level comment at the top of ConstrainedTracingSet is missing in 03bc, but 
is present in becb). Was the merge lossy/incorrect, or am I missing something?

- In ConstrainedTracingSet, it would help to list the variable defs at the top 
of the class -- currently they're in the middle of the file and are hard to 
find.

Original comment by bestchai on 10 Aug 2013 at 6:16

[GoogleCodeExporter]

1 & 3. Ok, will do.

2. Hm... I did have some issues when I was merging, so it's very possible that 
I messed that up.  I'll look at it and maybe try to merge becb into Issue 330 
again.

Original comment by tonyohm...@gmail.com on 10 Aug 2013 at 6:55

[GoogleCodeExporter]

Fixed in revision 23957c686a8b

Original comment by tonyohm...@gmail.com on 12 Aug 2013 at 5:47

[GoogleCodeExporter]

Merged into default with revision dab7f141cba9

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

• Changed state: Fixed