Commit f19d8f17 authored by hugues.jerome's avatar hugues.jerome
Browse files

* Update test outputs


git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@1374 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 1f6eec13
...@@ -13,7 +13,7 @@ requirement : mutexes ...@@ -13,7 +13,7 @@ requirement : mutexes
theorem mutexes is: TRUE theorem mutexes is: TRUE
requirement : latency requirement : latency
requirement : buses_rate requirement : buses_rate
lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on this single element. lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on element Bus_Set
lib.real:12:72 Backends: error : Property is false for instance 582 (shared.impl_a_bus) lib.real:12:72 Backends: error : Property is false for instance 582 (shared.impl_a_bus)
theorem buses_rate is: FALSE theorem buses_rate is: FALSE
lib.real:85:01 Backends: fatal error : requirements are not fulfilled lib.real:85:01 Backends: fatal error : requirements are not fulfilled
...@@ -7,26 +7,26 @@ all.aadl:197:07: warning: layer_unclassified references a component type ...@@ -7,26 +7,26 @@ all.aadl:197:07: warning: layer_unclassified references a component type
ocarina: Total: 0 error and 6 warnings ocarina: Total: 0 error and 6 warnings
pok_security execution pok_security execution
requirement : one_security_level_by_memory requirement : one_security_level_by_memory
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
lib.real:15:23 Backends: warning : cardinal of set is null lib.real:15:23 Backends: warning : cardinal of set b is null
lib.real:15:11 Backends: warning : use default boolean value of true lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
theorem one_security_level_by_memory is: TRUE theorem one_security_level_by_memory is: TRUE
requirement : bell_lapadula requirement : bell_lapadula
theorem bell_lapadula is: TRUE theorem bell_lapadula is: TRUE
...@@ -35,54 +35,54 @@ theorem biba is: TRUE ...@@ -35,54 +35,54 @@ theorem biba is: TRUE
requirement : mils_1 requirement : mils_1
theorem mils_1 is: TRUE theorem mils_1 is: TRUE
requirement : mils_2 requirement : mils_2
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
lib.real:117:20 Backends: warning : cardinal of set is null lib.real:117:20 Backends: warning : cardinal of set b_dst is null
lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:118:20 Backends: warning : cardinal of set is null lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
lib.real:119:20 Backends: warning : cardinal of set is null lib.real:119:20 Backends: warning : cardinal of set b_dst is null
lib.real:119:15 Backends: warning : use default float value of 0.0 lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
lib.real:120:20 Backends: warning : cardinal of set is null lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
lib.real:119:62 Backends: warning : use default float value of 0.0 lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
theorem mils_2 is: TRUE theorem mils_2 is: TRUE
requirement : scheduling_1 requirement : scheduling_1
theorem scheduling_1 is: TRUE theorem scheduling_1 is: TRUE
......
------------------------------------------ ------------------------------------------
------ Ocarina Petri Nets Generator ------ ------ Ocarina Petri Nets Generator ------
------------------------------------------ ------------------------------------------
test.aadl:12:03: warning: CPU references a component type test.aadl:12:03: warning: CPU references a component type
ocarina: Total: 0 error and 1 warning ocarina: Total: 0 error and 1 warning
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~ Timed Petri Nets ~~~~~~~~~~~ ~~~~~~~~~~~ Timed Petri Nets ~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
...@@ -28,7 +28,7 @@ property set Deployment is ...@@ -28,7 +28,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type Protocol : Deployment::Protocol_Type
applies to (system); applies to (system);
Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);
Execution_Platform : Deployment::Allowed_Execution_Platform Execution_Platform : Deployment::Allowed_Execution_Platform
applies to (processor); applies to (processor);
......
...@@ -28,7 +28,7 @@ property set Deployment is ...@@ -28,7 +28,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type Protocol : Deployment::Protocol_Type
applies to (system); applies to (system);
Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);
Execution_Platform : Deployment::Allowed_Execution_Platform Execution_Platform : Deployment::Allowed_Execution_Platform
applies to (processor); applies to (processor);
......
...@@ -28,7 +28,7 @@ property set Deployment is ...@@ -28,7 +28,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type Protocol : Deployment::Protocol_Type
applies to (system); applies to (system);
Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);
Execution_Platform : Deployment::Allowed_Execution_Platform Execution_Platform : Deployment::Allowed_Execution_Platform
applies to (processor); applies to (processor);
......
...@@ -28,7 +28,7 @@ property set Deployment is ...@@ -28,7 +28,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type Protocol : Deployment::Protocol_Type
applies to (system); applies to (system);
Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);
Execution_Platform : Deployment::Allowed_Execution_Platform Execution_Platform : Deployment::Allowed_Execution_Platform
applies to (processor); applies to (processor);
......
...@@ -28,7 +28,7 @@ property set Deployment is ...@@ -28,7 +28,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type Protocol : Deployment::Protocol_Type
applies to (system); applies to (system);
Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS); Allowed_Execution_Platform : type enumeration (Native, LEON_RTEMS, LEON_ORK, LEON_GNAT, ERC32_ORK, ARM_DSLINUX, ARM_N770, X86_RTEMS, X86_LINUXTASTE, MARTE_OS, VXWORKS);
Execution_Platform : Deployment::Allowed_Execution_Platform Execution_Platform : Deployment::Allowed_Execution_Platform
applies to (processor); applies to (processor);
......
...@@ -9,14 +9,14 @@ Usage: ...@@ -9,14 +9,14 @@ Usage:
-s Output Ocarina search directory, then exit -s Output Ocarina search directory, then exit
Scenario file options: Scenario file options:
-b build the generated application code -b Generate and build code from the AADL model
-z clean the generated application code -z Clean code generated from the AADL model
-ec execute the generated application code and -ec Execute the generated application code and
retrieve coverage information retrieve coverage information
-er execute the generated application code and -er Execute the generated application code and
verify that there is no regression verify that there is no regression
-p only parse and instantiate the application model -p Only parse and instantiate the application model
-c only perform schedulability analysis -c Only perform schedulability analysis
Advanced user options: Advanced user options:
-d Debug mode for developpers -d Debug mode for developpers
...@@ -25,6 +25,7 @@ Usage: ...@@ -25,6 +25,7 @@ Usage:
If a script is given, interpret it then exit. If a script is given, interpret it then exit.
-v Verbose mode for users -v Verbose mode for users
-x Parse AADL file as an AADL scenario file -x Parse AADL file as an AADL scenario file
-y Automatically load AADL files on demand
-f Parse predefined non standard property sets -f Parse predefined non standard property sets
-i Instantiate the AADL model -i Instantiate the AADL model
-r <name> The name of the instance tree root -r <name> The name of the instance tree root
...@@ -37,6 +38,7 @@ Usage: ...@@ -37,6 +38,7 @@ Usage:
Registered backends: Registered backends:
petri_nets petri_nets
boundt boundt
mast
polyorb_hi_ada polyorb_hi_ada
polyorb_qos_ada polyorb_qos_ada
polyorb_hi_c polyorb_hi_c
......
...@@ -7,7 +7,7 @@ Root_System Node_Id 6 ...@@ -7,7 +7,7 @@ Root_System Node_Id 6
Corresponding_Entity Node_Id 6 Corresponding_Entity Node_Id 6
Scope_Entity Node_Id 0 Scope_Entity Node_Id 0
Backend_Node Node_Id 0 Backend_Node Node_Id 0
Corresponding_Declaration Node_Id 1487 Corresponding_Declaration Node_Id 1488
Properties List_Id 0 Properties List_Id 0
Is_Private Boolean FALSE Is_Private Boolean FALSE
Features List_Id 0 Features List_Id 0
......
This diff is collapsed.
This diff is collapsed.
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