Test Case Generation Info:



Invariant restrictions:


Test Case 1 (Positive)

Formula: floor > 1


Preamble:

No preamble generated


Input data:
State
Variable Value
floor 2
Input Values
Parameter Value
This operation has no parameters
Expected results:
State
Variable Value
floor Unknown
Return Variables
Return Variable Value
This operation has no return variables

Test Case 2 (Positive)

Formula: not(floor > 1)


Preamble:

No preamble generated


Input data:
State
Variable Value
floor 1
Input Values
Parameter Value
This operation has no parameters
Expected results:
State
Variable Value
floor Unknown
Return Variables
Return Variable Value
This operation has no return variables

Infeasible Test Cases: