Commit 9c238e0a authored by Jerome Hugues's avatar Jerome Hugues

* Update refernce outputs

parent 46cd5ac2
-- This AADL model illustrates how to conduct schedulability analysis
-- using Cheddar, and then code generation of periodic tasks.
--
-- Two periodic tasks run in parrallel, without interaction. Tasks
-- parameters allows RMA analysis
--
-- $Id: rma.aadl 7042M 2010-03-30 07:55:51Z (local) $
package RMAAadl package RMAAadl
public public
with Deployment; with Deployment;
----------------- subprogram Hello_Spg_1
-- Subprograms --
-----------------
subprogram Hello_Spg_1
properties properties
source_language => (Ada95); source_language => (Ada95);
source_name => "Hello.Hello_Spg_1"; source_name => "Hello.Hello_Spg_1";
...@@ -100,6 +88,7 @@ subcomponents ...@@ -100,6 +88,7 @@ subcomponents
cpu_rm : processor cpurm.impl; cpu_rm : processor cpurm.impl;
properties properties
Actual_Processor_Binding => (reference (cpu_rm)) applies to node_a; Actual_Processor_Binding => (reference (cpu_rm)) applies to node_a;
end rma.ERC32; end rma.ERC32;
end RMAAadl; end RMAAadl;
...@@ -5,24 +5,24 @@ from ocarina import *; ...@@ -5,24 +5,24 @@ from ocarina import *;
def main (): def main ():
'''Test function''' '''Test function'''
for backends in Backends: result = add_real_library("rma.real") # load a file
print(backends); print "%r" % (result)
result = load("rma.aadl") # load a file
print "%r" % (result)
result = load("deployment.aadl") # load a file
print "%r" % (result)
result = analyze() # analyze models
print "Analysis result %r" % (result)
load("rma.aadl"); # load a file result = set_real_theorem ("rma_prop_def")
load("deployment.aadl"); # load a file result = generate (Backends.real_theorem)
result = analyze(); # analyze models print "REAL execution %r" % (result)
print "Analysis result %r" % (result); print ""
instantiate("rma.erc32"); # instantiate
generate (Backends.polyorb_hi_ada);
reset(); result = set_real_theorem ("rma_prop_def_2")
result = generate (Backends.real_theorem)
load("rma.aadl"); # load a file print "REAL execution %r" % (result)
load("deployment.aadl"); # load a file
analyze(); # analyze models
instantiate("rma.erc32"); # instantiate
generate (Backends.polyorb_hi_ada);
if __name__ == "__main__": if __name__ == "__main__":
main () main ()
sys.exit (0); # exit sys.exit (0) # exit
...@@ -5,6 +5,7 @@ test_real_exec_env_01.aadl:16:03: Warning: The value of source_language has been ...@@ -5,6 +5,7 @@ test_real_exec_env_01.aadl:16:03: Warning: The value of source_language has been
lib.real:12:17: warning: Unable to determine actualy returned type. lib.real:12:17: warning: Unable to determine actualy returned type.
lib.real:19:24: warning: Unable to determine actualy returned type. lib.real:19:24: warning: Unable to determine actualy returned type.
lib.real:33:03: warning: Returned integer value will be cast to a float at runtime lib.real:33:03: warning: Returned integer value will be cast to a float at runtime
lib.real:38:01 Backends: warning : Empty range set, returned value is 0.0
test_env_subtheorem_call_no_parameter execution test_env_subtheorem_call_no_parameter execution
------------------------------------- -------------------------------------
Evaluating theorem test_env_subtheorem_call_no_parameter Evaluating theorem test_env_subtheorem_call_no_parameter
...@@ -82,7 +83,6 @@ Evaluating theorem test_env_subtheorem_call_with_empty_domain ...@@ -82,7 +83,6 @@ Evaluating theorem test_env_subtheorem_call_with_empty_domain
* Iterate for variable: rma.erc32_node_a * Iterate for variable: rma.erc32_node_a
Content of set a_set (test_real_exec_env_01.aadl:133:12) is Content of set a_set (test_real_exec_env_01.aadl:133:12) is
Evaluating x Evaluating x
lib.real:38:01 Backends: warning : Empty range set, returned value is 0.0
value for x after evaluating sub_theorem_6 is 0.00000E+00 value for x after evaluating sub_theorem_6 is 0.00000E+00
=> Result: TRUE => Result: TRUE
......
...@@ -2,6 +2,8 @@ test_real_exec_05.aadl:10:03: Warning: source_language is not a list while the c ...@@ -2,6 +2,8 @@ test_real_exec_05.aadl:10:03: Warning: source_language is not a list while the c
test_real_exec_05.aadl:10:03: Warning: The value of source_language has been converted into a list. test_real_exec_05.aadl:10:03: Warning: The value of source_language has been converted into a list.
test_real_exec_05.aadl:16:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. test_real_exec_05.aadl:16:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
test_real_exec_05.aadl:16:03: Warning: The value of source_language has been converted into a list. test_real_exec_05.aadl:16:03: Warning: The value of source_language has been converted into a list.
test_real_exec_05.aadl:147:12 Backends: error : Property is false for instance 84 (rma.erc32_cpu_rm)
test_real_exec_05.aadl:170:12 Backends: error : Property is false for instance 84 (rma.erc32_cpu_rm)
variables_basis execution variables_basis execution
------------------------------------- -------------------------------------
Evaluating theorem variables_basis Evaluating theorem variables_basis
...@@ -60,7 +62,6 @@ Content of set threads (test_real_exec_05.aadl:141:14) is ...@@ -60,7 +62,6 @@ Content of set threads (test_real_exec_05.aadl:141:14) is
rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01
rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01
-> value for y is 6000000000.0 -> value for y is 6000000000.0
test_real_exec_05.aadl:147:12 Backends: error : Property is false for instance 84 (rma.erc32_cpu_rm)
=> Result: FALSE => Result: FALSE
theorem variables_iterative_expressions is: FALSE theorem variables_iterative_expressions is: FALSE
...@@ -77,7 +78,6 @@ Content of set threads (test_real_exec_05.aadl:158:14) is ...@@ -77,7 +78,6 @@ Content of set threads (test_real_exec_05.aadl:158:14) is
rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01 rma.erc32_node_a_task1: 20 component instance test_real_exec_05.aadl:27:01
rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01 rma.erc32_node_a_task2: 52 component instance test_real_exec_05.aadl:40:01
-> value for y is 7000000000.0 -> value for y is 7000000000.0
test_real_exec_05.aadl:170:12 Backends: error : Property is false for instance 84 (rma.erc32_cpu_rm)
=> Result: FALSE => Result: FALSE
theorem variables_imbricated_iterative_expressions is: FALSE theorem variables_imbricated_iterative_expressions is: FALSE
......
theorems.real:3:09 Backends: error : Property is false for instance 6 (a.impl)
test.aadl:9:02 Backends: error : requirements are not fulfilled for theorem test_theorem
test_theorem execution test_theorem execution
Processing requirement : required_theorem Processing requirement : required_theorem
------------------------------------- -------------------------------------
Evaluating theorem required_theorem Evaluating theorem required_theorem
* Iterate for variable: a.impl * Iterate for variable: a.impl
theorems.real:3:09 Backends: error : Property is false for instance 6 (a.impl)
=> Result: FALSE => Result: FALSE
theorem required_theorem is: FALSE theorem required_theorem is: FALSE
test.aadl:9:02 Backends: error : requirements are not fulfilled for theorem test_theorem
theorem test_theorem is: FALSE theorem test_theorem is: FALSE
......
theorems.real:9:10 Backends: error : Property is false for instance 6 (a.impl)
theorems.real:1:01 Backends: error : requirements of sub1 are not fulfilled
test.aadl:8:05 Backends: error : requirements are not fulfilled for theorem test
test execution test execution
Processing requirement : sub1 Processing requirement : sub1
Processing requirement : sub2 Processing requirement : sub2
...@@ -5,12 +8,10 @@ Processing requirement : sub2 ...@@ -5,12 +8,10 @@ Processing requirement : sub2
Evaluating theorem sub2 Evaluating theorem sub2
* Iterate for variable: a.impl * Iterate for variable: a.impl
theorems.real:9:10 Backends: error : Property is false for instance 6 (a.impl)
=> Result: FALSE => Result: FALSE
theorem sub2 is: FALSE theorem sub2 is: FALSE
theorems.real:1:01 Backends: error : requirements of sub1 are not fulfilled
------------------------------------- -------------------------------------
Evaluating theorem sub1 Evaluating theorem sub1
...@@ -19,7 +20,6 @@ Evaluating theorem sub1 ...@@ -19,7 +20,6 @@ Evaluating theorem sub1
theorem sub1 is: FALSE theorem sub1 is: FALSE
test.aadl:8:05 Backends: error : requirements are not fulfilled for theorem test
theorem test is: FALSE theorem test is: FALSE
test.real:9:09 Backends: error : Property is false for instance 6 (a.impl)
test.real:1:01 Backends: error : requirements of sub1 are not fulfilled
test.aadl:26:09 Backends: error : requirements are not fulfilled for theorem test
test execution test execution
Processing requirement : sub1 Processing requirement : sub1
Processing requirement : sub2 Processing requirement : sub2
...@@ -5,7 +8,6 @@ Processing requirement : sub2 ...@@ -5,7 +8,6 @@ Processing requirement : sub2
Evaluating theorem sub2 Evaluating theorem sub2
* Iterate for variable: a.impl * Iterate for variable: a.impl
test.real:9:09 Backends: error : Property is false for instance 6 (a.impl)
=> Result: FALSE => Result: FALSE
theorem sub2 is: FALSE theorem sub2 is: FALSE
...@@ -25,7 +27,6 @@ Evaluating theorem sub3 ...@@ -25,7 +27,6 @@ Evaluating theorem sub3
theorem sub3 is: TRUE theorem sub3 is: TRUE
test.real:1:01 Backends: error : requirements of sub1 are not fulfilled
------------------------------------- -------------------------------------
Evaluating theorem sub1 Evaluating theorem sub1
...@@ -40,7 +41,6 @@ Evaluating theorem sub1 ...@@ -40,7 +41,6 @@ Evaluating theorem sub1
theorem sub1 is: FALSE theorem sub1 is: FALSE
test.aadl:26:09 Backends: error : requirements are not fulfilled for theorem test
theorem test is: FALSE theorem test is: FALSE
...@@ -2,6 +2,8 @@ validation.aadl:13:03: Warning: source_language is not a list while the correspo ...@@ -2,6 +2,8 @@ validation.aadl:13:03: Warning: source_language is not a list while the correspo
validation.aadl:13:03: Warning: The value of source_language has been converted into a list. validation.aadl:13:03: Warning: The value of source_language has been converted into a list.
validation.aadl:20:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list. validation.aadl:20:03: Warning: source_language is not a list while the corresponding property name at programming_properties.aadl:61:02 is a list.
validation.aadl:20:03: Warning: The value of source_language has been converted into a list. validation.aadl:20:03: Warning: The value of source_language has been converted into a list.
validation.aadl:135:99 Backends: error : Property is false for instance 122 (mysystem.local_ram)
validation.aadl:151:16 Backends: error : Property is false for instance 13 (mysystem.local_node)
contains_memories execution contains_memories execution
------------------------------------- -------------------------------------
Evaluating theorem contains_memories Evaluating theorem contains_memories
...@@ -21,7 +23,6 @@ Evaluating theorem check_memory_and_process_mem ...@@ -21,7 +23,6 @@ Evaluating theorem check_memory_and_process_mem
* Iterate for variable: mysystem.local_ram * Iterate for variable: mysystem.local_ram
Content of set prs (validation.aadl:133:28) is Content of set prs (validation.aadl:133:28) is
mysystem.local_node: 13 component instance validation.aadl:87:01 mysystem.local_node: 13 component instance validation.aadl:87:01
validation.aadl:135:99 Backends: error : Property is false for instance 122 (mysystem.local_ram)
=> Result: FALSE => Result: FALSE
theorem check_memory_and_process_mem is: FALSE theorem check_memory_and_process_mem is: FALSE
...@@ -35,7 +36,6 @@ Evaluating theorem check_thread_and_process_mem ...@@ -35,7 +36,6 @@ Evaluating theorem check_thread_and_process_mem
Content of set thrs (validation.aadl:144:28) is Content of set thrs (validation.aadl:144:28) is
mysystem.local_node_p1: 20 component instance validation.aadl:32:01 mysystem.local_node_p1: 20 component instance validation.aadl:32:01
mysystem.local_node_p2: 60 component instance validation.aadl:51:01 mysystem.local_node_p2: 60 component instance validation.aadl:51:01
validation.aadl:151:16 Backends: error : Property is false for instance 13 (mysystem.local_node)
=> Result: FALSE => Result: FALSE
theorem check_thread_and_process_mem is: FALSE theorem check_thread_and_process_mem is: FALSE
......
...@@ -17,11 +17,12 @@ Usage: ocarina [switches] <aadl_files> ...@@ -17,11 +17,12 @@ Usage: ocarina [switches] <aadl_files>
-i Instantiate the model -i Instantiate the model
-x Parse AADL file as an AADL scenario file -x Parse AADL file as an AADL scenario file
-g ARG Generate code using Ocarina backend 'ARG' -g ARG Generate code using Ocarina backend 'ARG'
--list-backends List available backends
-b Compile generated code -b Compile generated code
-z Clean code generated -z Clean code generated
-k ARG Set POK flavor (arinc653/deos/pok/vxworks) -k ARG Set POK flavor (arinc653/deos/pok/vxworks)
-t Run Ocarina in terminal interactive mode -t Run Ocarina in terminal interactive mode
-real_theorem ARG Name of the main theorem to evaluate -real_theorem ARG Name of the main REAL theorem to evaluate
-real_lib ARG Add external library of REAL theorems -real_lib ARG Add external library of REAL theorems
-real_continue_eval Continue evaluation of REAL theorems after first failure (REAL backend) -real_continue_eval Continue evaluation of REAL theorems after first failure (REAL backend)
-boundt_process ARG Generate .tpo file for process ARG (Bound-T backend) -boundt_process ARG Generate .tpo file for process ARG (Bound-T backend)
......
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