search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Error in Column AA (Step 25) in jlustre2excel Output #37

Closed manthonyaiello closed 7 years ago

manthonyaiello commented 7 years ago

Column AA — which corresponds to the 25th step — in jlustre2excel's output appears to be consistently incorrect.

For example, for this Lustre,

node triggers(a : bool; b : bool) returns (holds : bool);
let
   holds = (b and (a or (false -> (pre holds))));
tel;

The spreadsheet generated has the following formulas for Z, AA, and AB:

=IF(OR(IF(ISERROR(Y7),FALSE,Y7=""),IF(ISERROR(Z3),FALSE,Z3=""),IF(ISERROR(Z4),FALSE,Z4="")),"",AND(Z4,OR(Z3,(Y7))))
=IF(OR(IF(ISERROR(AA3),FALSE,AA3=""),IF(ISERROR(AA4),FALSE,AA4=""),IF(ISERROR(Z7),FALSE,Z7="")),"",AND(AA4,OR(AA3,(Z7))))
=IF(OR(IF(ISERROR(AA7),FALSE,AA7=""),IF(ISERROR(AB3),FALSE,AB3=""),IF(ISERROR(AB4),FALSE,AB4="")),"",AND(AB4,OR(AB3,(AA7))))

Nearly every cell reference in column AA is incorrect.

Note — Excel identifies this problem immediately with its "this cell's formula doesn't match its neighbors" warning, which is frankly one of the cleverest things I've ever seen Microsoft do. No heroics on my part, here. :)

agacek commented 7 years ago

I believe the output is still correct, it's just ordered differently due to the name change at 26 columns. One can reorder:

=IF(OR(IF(ISERROR(AA3),FALSE,AA3=""),IF(ISERROR(AA4),FALSE,AA4=""),IF(ISERROR(Z7),FALSE,Z7="")),"",AND(AA4,OR(AA3,(Z7))))

to

=IF(OR(IF(ISERROR(Z7),FALSE,Z7=""),IF(ISERROR(AA3),FALSE,AA3=""),IF(ISERROR(AA4),FALSE,AA4="")),"",AND(AA4,OR(AA3,(Z7))))

Still, it's not good for excel to complain. I'll have to try to find a better way of ordering things. Right now it's just alphabetic I think.