file format error returned by dReach

[rachelwang]

why and when dreal returns with the following information?

dReal Options:
>> file format error: The last mode of the given path [1, 2, 2, 2, 2] is 2 which is not an element of [1], the list of modes in the goal section of the given hybrid system model.

[rachelwang]

This one as well:

Uncaught exception: Bmc.SMTException("time should be defined once and only once.")

[soonhokong]

why and when dreal returns with the following information?

bmc program takes three input parameters:

• a model, say model.drh.
• an unrolling bound k, let's say k = 3.
• a path to check: let's say [1, 2, 2, 2] which means 1 -> 2 -> 2 -> 2

The error message indicates that your model (.drh file) has the following specifications:

• init_mode = 1
• goal_mode = 1

and the provided path [1, 2, 2, 2] is not satisfiable because the final mode in the path is 2, not 1.

Now, you may have a question, "I haven't really provided a path to dReach. Then why do I have the error?"

The answer is that for now dReach explicitly enumerates all possible paths from the given model and run bmc for paths, one by one. Actually, dReach should not enumerate the path [1,2,2,2] since it's obviously unreachable. I think this is a bug. Can you give me the drh file that you tried with? I'll fix the bug later.

This one as well:

Please file a separate issue for this one with the .drh that you provided.

[soonhokong]

BTW, this explicit path enumeration is of course not the ideal thing to do. @scungao, @danbryce, and I are working on a better way to handle the problem.

[soonhokong]

8320e93de1507c5e38b73cb804ebe44fb2c3dabf fixes the problem of bmc generating unfeasible paths. @rachelwang, please try to use this one and report errors if any.