XSTS-cli: Verifying a model with syntax errors should fail

[arminzavada]

Theta version: docker 6.5.2

XSTS-cli ignores certain syntactical errors if the lexer can construct something meaningful out of the input model.

Example input:

var x : integer = 0
trans {
    choice {
        assume (x == 2);
    } else {
        x := 10;
    }
}
init {}
env {}
prop {
    x != 0
}

Expected outcome: Theta fails since else can't come after 'choice'
Actual outcome: Theta outputs the syntax errors, and continues by "covering" the 'else' branch.

stderr:

line 8:6 extraneous input 'else' expecting {'if', 'havoc', 'assume', 'choice', 'for', '{', '}', 'local', ID}

stdout:

Iteration 1
| Checking abstraction...
|  |  (Re)initializing ARG...done
|  |  Building ARG...done
| Checking abstraction done, result: (AbstractorResult Unsafe)
| Refining abstraction...
|  |  Checking trace...done, result: (ExprTraceStatus Feasible)
Refining abstraction done, result: (RefinerResult Unsafe)
! Precision did NOT change in this iteration
(SafetyResult Unsafe Trace length: 0)

CEX:

(XstsStateSequence (XstsState pre_init last_env (ExplState (x 0))))

Return code: 0

Proposed solution:

Theta should throw an exception if there are any syntactical errors.