Commit bcfd31d9 authored by jhugues's avatar jhugues

* Added real_requires_3 data



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@5747 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent fdbddadf
AADL_VERSION=-aadlv2
OCARINA_FLAGS=-q -real_continue_eval -g real_theorem -real_lib test.real -r a.impl
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;
\ No newline at end of file
test execution
Processing requirement : sub1
Processing 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
Processing 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 of sub1 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: FALSE
test.aadl:26:09 Backends: error : requirements are not fulfilled for theorem test
theorem test is: FALSE
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;
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment