VerifiableRobotics / LTLMoP

A toolkit for designing and implementing LTL-based task specifications.
http://ltlmop.github.io
GNU General Public License v3.0
56 stars 69 forks source link

Extra & in LTL file if no environment constraints #12

Closed ConstantineLignos closed 12 years ago

ConstantineLignos commented 12 years ago

Reproduction steps:

  1. Checkout latest slurp-dev (cc96ed4).
  2. Run python specEditor.py examples/slurptest/slurptest_unreal.spec
  3. Compile

Expected: Spec compiles but is unrealizable. Actual: Compilation fails with:

Creating automaton...
    line 10:1 no viable alternative at input ')'
    Exception in thread "main" java.lang.Exception: Cannot parse specification "null".

When I look at the .ltl file, I see:

LTLSPEC -- Assumptions
        (
        TRUE & [](TRUE) & []<>(TRUE)
                &

        );

It looks like that extra & is killing it.