Create unit tests for all requirement patterns

[danieldietsch]

We need to create unit tests for all patterns s.t. we can be more confident that the formalization is interpreted correctly.

The current pattern grammar is

2019-06-19 req parser simplified grammar  
 
REQ      ::= REQID SCOPE ,? PATTERN .?
REQID    ::= ID:
SCOPE    ::= Globally
           | Before EXPR 
           | After EXPR
           | Between EXPR and EXPR
           | After EXPR until EXPR
PATTERN  ::= It is never the case that EXPR holds
           | It is always the case that EXPR holds 
           | It is always the case that if EXPR holds ,? then EXPR holds as well
           | EXPR eventually holds
           | Transition to states in which EXPR holds occur at most twice
           | It is always the case that ORDER 
           | It is always the case that REALTIME
ORDER    ::=          
           | If EXPR holds ,? then EXPR previously held
           | If EXPR holds and is succeded by EXPR ,? then EXPR previously held
           | If EXPR holds ,? then EXPR previously held and was preceeded by EXPR
           | If EXPR holds ,? then EXPR eventually holds
           | If EXPR holds ,? then EXPR eventually holds and is succeeded by EXPR
           | If EXPR holds and is succeeded by EXPR ,? then EXPR eventually holds after EXPR
           | If EXPR holds ,? then EXPR eventually holds and is succeeded by EXPR where EXPR does not hold between EXPR and EXPR
           | If EXPR holds ,? then EXPR toggles EXPR
REALTIME ::= Once EXPR becomes satisfied ,? it holds for at least DURATION
           | Once EXPR becomes satisfied ,? it holds for less than DURATION
           | EXPR holds at least every DURATION
           | If EXPR holds ,? then EXPR holds after at most DURATION
           | If EXPR holds for at least DURATION ,? then EXPR holds afterwards for at least DURATION
           | If EXPR holds for at least DURATION ,? then EXPR holds afterwards
           | If EXPR holds ,? then EXPR holds after at most DURATION for at least DURATION
           | If EXPR holds ,? then EXPR holds for at least DURATION
           | If EXPR holds ,? then there is at least one execution sequence such that EXPR holds after at most DURATION
           | After EXPR holds for DURATION ,? then EXPR holds
           | If EXPR holds ,? then EXPR toggles EXPR at most DURATION later

Unit tests should cover:

• Parsing (for each pattern one test)
• rt-inconsistency with 2 different patterns, also with necessitating the transitive hull (via invariants)
• vacuity with different patterns, also with transitive hull
• const-handling
• disjunctive invariants

There is already a syntax to describe expected results defined by ReqCheckerTestResultDecider (all implementation is found in ReqCheckerRegressionTestSuite).

Example:
#TestSpec: rt-inconsistent:req1+req2; vacuous:; inconsistent:; results: 4

specifies that the result of this test should find that req1 and req2 are rt-inconsistent, that there are no vacuous requirements, and that 4 results are produced.

Look at already existing examples in https://github.com/ultimate-pa/ultimate/tree/dev/trunk/examples/Requirements/regression