Ocarina reports incorrect theorem result with nested theorems with -real_continue_eval

[philip-alldredge]

In the below example, theorem "test", and "sub1" both report true even though a required theorem of sub2, sub1 fails.

bug.aadl package BugTest public system A end A;

system implementation A.impl
annex real_specification {**
    theorem test
    foreach s in system_set do
        requires (sub1);
        check (1 = 1);
    end test;

**}; end A.impl;

end BugTest;

bug.real

theorem sub1 foreach s in System_Set do requires(sub2); check (1 = 1); end sub1;

theorem sub2 foreach s in System_Set do check (1 = 0); end sub2;

[yoogx]

Bug solved, new output is now

neraka-2% less test.aadl.out test execution requirement : sub1

requirement : sub2

Evaluating theorem sub2

• Iterate for variable: a.impl theorems.real:9:10 Backends: error : Property is false for instance 6 (a.impl) => Result: FALSE

theorem sub2 is: FALSE

theorems.real:1:01 Backends: error : requirements are not fulfilled

Evaluating theorem sub1

• Iterate for variable: a.impl => Result: TRUE

theorem sub1 is: TRUE

test.aadl:8:05 Backends: error : requirements are not fulfilled for theorem test

theorem test is: FALSE

[philip-alldredge]

(Removed comment pending further testing)

[philip-alldredge]

Confirmed that it works as described. Please disregard my previous message if github sent it out before I removed it.

I do however find it odd/inconsistent that sub1 reports TRUE. I would of expected a "requirements are not fulfilled for theorem sub1".

Thanks for the quick fix.

[yoogx]

Well, it is odd, but it was part of your requirements: report a theorem true even if a requires clause is false. I may have interpreted it wrongly. The point was; you wanted to evaluated the theorem even if the requires clause returned false. As a result, we return the result of the theorem, and a warning that the requires is false

Just let me know what you prefer. I can modify the code to report false in this case.

[philip-alldredge]

When I referred to inconsistency I was referring to theorem "sub1" reporting TRUE when it's requirements failed and theorem "Test" returning FALSE because it's requirements failed. I apologize for the confusion I apparently have caused.

What I would like to see: If a requirement fails, the theorem should fail.

All the requirements to be evaluated regardless of whether a previous one was false.
    I believe this is part of the the original confusion. I don't want the entire theorem to be evaluated or affect the result, but I would like all the requirements to be evaluated in the case of multiple requirements.
    Example: requires(sub1 and sub2) - Both should be evaluated even if sub1 is false.

I hope this clears things up.

[philip-alldredge]

Reopened issue for further discussion. I didn't realize I had closed it.

[yoogx]

Can you tell me, from the example and your requirements, what is the output you expect?

[philip-alldredge]

Okay. I have expanded the new example because there is something else I would like to request to be changed and I thought a comprehensive example might be best. The three things I would like to see: Report that a theorem is false because its requirements failed when a required theorem fails. Continue evaluating the theorem for all instances even when a instance has been found that makes the instance false. Evaluate all requirements regardless of whether a previous one failed.

test.aadl:

package Test
public
    system B
    end B;

    system implementation B.impl
    end B.impl;

    system C
    end C;

    system implementation C.impl
    properties
        Priority => 5;
    end C.impl;

    system A
    end A;

    system implementation A.impl
    subcomponents
        b1 : system B.impl;
        c1 : system C.impl;

    annex real_specification {**
        theorem test
        foreach s in system_set do
            requires (sub1);
            check (1 = 1);
        end test;
   **};
    end A.impl;

end Test;

test.real:

theorem sub1
  foreach s in System_Set do
  requires(sub2 and sub3);
  check (1 = 1);
end sub1;

theorem sub2
  foreach s in System_Set do
  check (Property_Exists(s, "Priority"));
end sub2;

theorem sub3
  foreach s in System_Set do
  check (1 = 1);
end sub3;

Current Output:

test execution
requirement : sub1
requirement : sub2
-------------------------------------
Evaluating theorem sub2

 * Iterate for variable: a.impl
test.real:9:09 Backends: error : Property is false for instance 6 (a.impl)
 => Result: FALSE

theorem sub2 is: FALSE

requirement : sub3
-------------------------------------
Evaluating theorem sub3

 * Iterate for variable: a.impl
 => Result: TRUE

 * Iterate for variable: a.impl_b1
 => Result: TRUE

 * Iterate for variable: a.impl_c1
 => Result: TRUE

theorem sub3 is: TRUE

test.real:1:01 Backends: error : requirements are not fulfilled
-------------------------------------
Evaluating theorem sub1

 * Iterate for variable: a.impl
 => Result: TRUE

 * Iterate for variable: a.impl_b1
 => Result: TRUE

 * Iterate for variable: a.impl_c1
 => Result: TRUE

theorem sub1 is: TRUE

test.aadl:26:03 Backends: error : requirements are not fulfilled for theorem test

theorem test is: FALSE

Desired Output:

test execution
requirement : sub1
requirement : sub2
-------------------------------------
Evaluating theorem sub2

 * Iterate for variable: a.impl
test.real:9:09 Backends: error : Property is false for instance 6 (a.impl)
 => Result: FALSE

 * Iterate for variable: a.impl_b1
 test.real:9:09 Backends: error : Property is false for instance ? (a.impl_b1)
 => Result: FALSE

 * Iterate for variable: a.impl_c1
 => Result: TRUE

theorem sub2 is: FALSE

requirement : sub3
-------------------------------------
Evaluating theorem sub3

 * Iterate for variable: a.impl
 => Result: TRUE

 * Iterate for variable: a.impl_b1
 => Result: TRUE

 * Iterate for variable: a.impl_c1
 => Result: TRUE

theorem sub3 is: TRUE

-------------------------------------
Evaluating theorem sub1

test.real:1:01 Backends: error : requirements are not fulfilled

theorem sub1 is: FALSE

test.aadl:26:03 Backends: error : requirements are not fulfilled for theorem test

theorem test is: FALSE

[yoogx]

Hi Phil, this is now corrected in Ocarina nightly build, you may test this tomorrow.