Skip to content

GitLab

Commit b26ec36a authored by yoogx's avatar yoogx
Browse files

Merge branch 'ocarina_svn_enis'

parents 9f89dde3 c0aa7c2d
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 4833 additions and 84 deletions
autotest.sh
View file @ b26ec36a
......@@ -470,9 +470,9 @@ if test ${dotests} = "true" ; then
# failures=`expr ${failures} + 1`
else
./`basename ${file} .adb` >${actual_output} 2>&1
command="./`basename ${file} .adb`"
result=$?
OCARINA_PATH="`which ocarina`" ./`basename ${file} .adb` >${actual_output} 2>&1
command="./`basename ${file} .adb`"
result=$?
if test -r ${expected_output} ; then
${scriptdir}/tools/compare.py \
......
examples/real/security/all.aadl.out
View file @ b26ec36a
......@@ -146,48 +146,48 @@ Evaluating theorem bell_lapadula
* Iterate for variable: main.i_node1_partition_topsecret
Content of set vp1 (lib.real:27:14) is
main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04
main.i_node1_runtime_topsecret: 53 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:31:17) is
main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04
main.i_node2_partition_topsecret: 465 component instance all.aadl:138:04
Content of set vp2 (lib.real:33:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_dst (lib.real:35:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_secret
Content of set vp1 (lib.real:27:14) is
main.i_node1_runtime_secret: 28 component instance all.aadl:156:04
main.i_node1_runtime_secret: 30 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:31:17) is
main.i_node2_partition_secret: 483 component instance all.aadl:138:04
main.i_node2_partition_secret: 537 component instance all.aadl:138:04
Content of set vp2 (lib.real:33:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_dst (lib.real:35:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_unclassified
Content of set vp1 (lib.real:27:14) is
main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04
main.i_node1_runtime_unclassified: 72 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:31:17) is
main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04
main.i_node2_partition_unclassified: 606 component instance all.aadl:138:04
Content of set vp2 (lib.real:33:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_dst (lib.real:35:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
=> Result: TRUE
* Iterate for variable: main.i_node2_partition_topsecret
Content of set vp1 (lib.real:27:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:31:17) is
Content of set vp2 (lib.real:33:14) is
Content of set b_dst (lib.real:35:16) is
......@@ -195,9 +195,9 @@ Content of set b_dst (lib.real:35:16) is
* Iterate for variable: main.i_node2_partition_secret
Content of set vp1 (lib.real:27:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:31:17) is
Content of set vp2 (lib.real:33:14) is
Content of set b_dst (lib.real:35:16) is
......@@ -205,9 +205,9 @@ Content of set b_dst (lib.real:35:16) is
* Iterate for variable: main.i_node2_partition_unclassified
Content of set vp1 (lib.real:27:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_src (lib.real:29:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:31:17) is
Content of set vp2 (lib.real:33:14) is
Content of set b_dst (lib.real:35:16) is
......@@ -221,48 +221,48 @@ Evaluating theorem biba
* Iterate for variable: main.i_node1_partition_topsecret
Content of set vp1 (lib.real:51:14) is
main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04
main.i_node1_runtime_topsecret: 53 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:55:17) is
main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04
main.i_node2_partition_topsecret: 465 component instance all.aadl:138:04
Content of set vp2 (lib.real:57:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_dst (lib.real:59:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_secret
Content of set vp1 (lib.real:51:14) is
main.i_node1_runtime_secret: 28 component instance all.aadl:156:04
main.i_node1_runtime_secret: 30 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:55:17) is
main.i_node2_partition_secret: 483 component instance all.aadl:138:04
main.i_node2_partition_secret: 537 component instance all.aadl:138:04
Content of set vp2 (lib.real:57:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_dst (lib.real:59:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_unclassified
Content of set vp1 (lib.real:51:14) is
main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04
main.i_node1_runtime_unclassified: 72 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:55:17) is
main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04
main.i_node2_partition_unclassified: 606 component instance all.aadl:138:04
Content of set vp2 (lib.real:57:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_dst (lib.real:59:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
=> Result: TRUE
* Iterate for variable: main.i_node2_partition_topsecret
Content of set vp1 (lib.real:51:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:55:17) is
Content of set vp2 (lib.real:57:14) is
Content of set b_dst (lib.real:59:16) is
......@@ -270,9 +270,9 @@ Content of set b_dst (lib.real:59:16) is
* Iterate for variable: main.i_node2_partition_secret
Content of set vp1 (lib.real:51:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:55:17) is
Content of set vp2 (lib.real:57:14) is
Content of set b_dst (lib.real:59:16) is
......@@ -280,9 +280,9 @@ Content of set b_dst (lib.real:59:16) is
* Iterate for variable: main.i_node2_partition_unclassified
Content of set vp1 (lib.real:51:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_src (lib.real:53:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:55:17) is
Content of set vp2 (lib.real:57:14) is
Content of set b_dst (lib.real:59:16) is
......@@ -296,48 +296,48 @@ Evaluating theorem mils_1
* Iterate for variable: main.i_node1_partition_topsecret
Content of set vp1 (lib.real:73:14) is
main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04
main.i_node1_runtime_topsecret: 53 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:77:17) is
main.i_node2_partition_topsecret: 416 component instance all.aadl:138:04
main.i_node2_partition_topsecret: 465 component instance all.aadl:138:04
Content of set vp2 (lib.real:79:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_dst (lib.real:81:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_secret
Content of set vp1 (lib.real:73:14) is
main.i_node1_runtime_secret: 28 component instance all.aadl:156:04
main.i_node1_runtime_secret: 30 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:77:17) is
main.i_node2_partition_secret: 483 component instance all.aadl:138:04
main.i_node2_partition_secret: 537 component instance all.aadl:138:04
Content of set vp2 (lib.real:79:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_dst (lib.real:81:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
=> Result: TRUE
* Iterate for variable: main.i_node1_partition_unclassified
Content of set vp1 (lib.real:73:14) is
main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04
main.i_node1_runtime_unclassified: 72 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:77:17) is
main.i_node2_partition_unclassified: 547 component instance all.aadl:138:04
main.i_node2_partition_unclassified: 606 component instance all.aadl:138:04
Content of set vp2 (lib.real:79:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_dst (lib.real:81:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
=> Result: TRUE
* Iterate for variable: main.i_node2_partition_topsecret
Content of set vp1 (lib.real:73:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set p_dest (lib.real:77:17) is
Content of set vp2 (lib.real:79:14) is
Content of set b_dst (lib.real:81:16) is
......@@ -345,9 +345,9 @@ Content of set b_dst (lib.real:81:16) is
* Iterate for variable: main.i_node2_partition_secret
Content of set vp1 (lib.real:73:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set p_dest (lib.real:77:17) is
Content of set vp2 (lib.real:79:14) is
Content of set b_dst (lib.real:81:16) is
......@@ -355,9 +355,9 @@ Content of set b_dst (lib.real:81:16) is
* Iterate for variable: main.i_node2_partition_unclassified
Content of set vp1 (lib.real:73:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_src (lib.real:75:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set p_dest (lib.real:77:17) is
Content of set vp2 (lib.real:79:14) is
Content of set b_dst (lib.real:81:16) is
......@@ -371,9 +371,9 @@ Evaluating theorem mils_2
* Iterate for variable: main.i_node1_partition_topsecret
Content of set vp1 (lib.real:98:14) is
main.i_node1_runtime_topsecret: 48 component instance all.aadl:156:04
main.i_node1_runtime_topsecret: 53 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......@@ -383,9 +383,9 @@ Content of set b_cnx (lib.real:110:16) is
* Iterate for variable: main.i_node1_partition_secret
Content of set vp1 (lib.real:98:14) is
main.i_node1_runtime_secret: 28 component instance all.aadl:156:04
main.i_node1_runtime_secret: 30 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......@@ -395,9 +395,9 @@ Content of set b_cnx (lib.real:110:16) is
* Iterate for variable: main.i_node1_partition_unclassified
Content of set vp1 (lib.real:98:14) is
main.i_node1_runtime_unclassified: 64 component instance all.aadl:156:04
main.i_node1_runtime_unclassified: 72 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......@@ -407,9 +407,9 @@ Content of set b_cnx (lib.real:110:16) is
* Iterate for variable: main.i_node2_partition_topsecret
Content of set vp1 (lib.real:98:14) is
main.i_node2_runtime_topsecret: 139 component instance all.aadl:156:04
main.i_node2_runtime_topsecret: 160 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_topsecret: 727 component instance all.aadl:15:04
main.i_rtbus_layer_topsecret: 821 component instance all.aadl:15:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......@@ -419,9 +419,9 @@ Content of set b_cnx (lib.real:110:16) is
* Iterate for variable: main.i_node2_partition_secret
Content of set vp1 (lib.real:98:14) is
main.i_node2_runtime_secret: 124 component instance all.aadl:156:04
main.i_node2_runtime_secret: 142 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_secret: 735 component instance all.aadl:10:04
main.i_rtbus_layer_secret: 830 component instance all.aadl:10:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......@@ -431,9 +431,9 @@ Content of set b_cnx (lib.real:110:16) is
* Iterate for variable: main.i_node2_partition_unclassified
Content of set vp1 (lib.real:98:14) is
main.i_node2_runtime_unclassified: 154 component instance all.aadl:156:04
main.i_node2_runtime_unclassified: 178 component instance all.aadl:156:04
Content of set b_src (lib.real:100:16) is
main.i_rtbus_layer_unclassified: 743 component instance all.aadl:5:04
main.i_rtbus_layer_unclassified: 839 component instance all.aadl:5:04
Content of set cnx (lib.real:102:14) is
Content of set p_dest (lib.real:104:17) is
Content of set vp2 (lib.real:106:14) is
......
projects/Makefile.am
View file @ b26ec36a
......@@ -57,11 +57,14 @@ TREE_PIDL_SPECS = src/core/tree/ocarina-me_aadl-aadl_tree-nodes.idl \
src/core/tree/ocarina-me_aadl-aadl_instances-nodes.idl \
src/core/tree/ocarina-me_aadl_ba-ba_tree-nodes.idl \
src/core/tree/ocarina-me_real-real_tree-nodes.idl \
src/core/tree/ocarina-me_ao4aadl-ao4aadl_tree-nodes.idl \
src/core/tree/ocarina-me_aadl_ema-ema_tree-nodes.idl \
src/backends/ocarina-backends-ada_tree-nodes.idl \
src/backends/ocarina-backends-c_tree-nodes.idl \
src/backends/ocarina-backends-asn1_tree-nodes.idl \
src/backends/ocarina-backends-xml_tree-nodes.idl \
src/backends/ocarina-backends-pn-nodes.idl \
src/backends/ocarina-backends-lnt-nodes.idl \
src/backends/ocarina-backends-mast_tree-nodes.idl
TREE_ADA_SPECS = ${addprefix $(top_builddir)/, $(TREE_PIDL_SPECS:.idl=.ads)}
......
projects/ocarina-frontends.gpr
View file @ b26ec36a
......@@ -6,7 +6,7 @@
-- --
-- P r o j e c t --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2015 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2016 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -39,6 +39,8 @@ project Ocarina.Frontends is
for Source_Dirs use
(Src_Dir & "/aadl",
Src_Dir & "/aadl_ba",
Src_Dir & "/aadl_ema",
Src_Dir & "/ao4aadl",
Src_Dir & "/real");
for Object_Dir use Build_Dir & "/objects";
for Library_Dir use Build_Dir & "/libs";
......
resources/AADLv2/errorlibrary.aadl 0 → 100644
View file @ b26ec36a
package ErrorLibrary
public
annex EMV2 {**
error types
CommonErrors: type set { ServiceError, TimingRelatedError, ValueRelatedError, ReplicationError,
ConcurrencyError};
--service related errors
ServiceError: type;
ItemOmission: type extends ServiceError;
ServiceOmission: type extends ServiceError;
SequenceOmission: type extends ServiceError;
TransientServiceOmission: type extends SequenceOmission;
LateServiceStart: type extends SequenceOmission;
EarlyServiceTermination: type extends SequenceOmission;
BoundedOmissionInterval: type extends SequenceOmission;
ItemComission: type extends ServiceError;
ServiceCommission: type extends ServiceError;
SequenceCommission: type extends ServiceError;
EarlyServiceStart: type extends SequenceCommission;
LateServiceTermination: type extends SequenceCommission;
--timing related errors
TimingRelatedError: type set {ItemTimingError, SequenceTimingError, ServiceTimingError};
-- Item timing errors
ItemTimingError: type;
EarlyDelivery: type extends ItemTimingError;
LateDelivery: type extends ItemTimingError;
--Rate/sequence timing errors
SequenceTimingError: type;
HighRate: type extends SequenceTimingError;
LowRate: type extends SequenceTimingError;
RateJitter: type extends SequenceTimingError;
-- Service timing error
ServiceTimingError: type;
DelayedService: type extends ServiceTimingError;
EarlyService: type extends ServiceTimingError;
-- aliases for timing errors
TimingError renames type ItemTimingError; -- legacy
RateError renames type SequenceTimingError;
EarlyData renames type HighRate;
LateData renames type LowRate;
ServiceTimeShift renames type ServiceTimingError;
--value related errors
ValueRelatedError: type set {ItemValueError, SequenceValueError, ServiceValueError};
-- item value errors
ItemValueError: type;
UndetectableValueError: type extends ItemValueError;
DetectableValueError: type extends ItemValueError;
OutOfRange: type extends DetectableValueError;
BelowRange: type extends OutOfRange;
AboveRange: type extends OutOfRange;
OutOfBounds: type extends DetectableValueError;
-- sequence errors
SequenceValueError: type;
BoundedValueChange: type extends SequenceError;
StuckValue: type extends SequenceError;
OutOfOrder: type extends SequenceError;
ServiceValueError: type;
OutOfCalibration: type extends ServiceValueError;
-- Common aliases for value related errors
ValueError renames type ItemValueError;
IncorrectValue renames type ItemValueError;
ValueCorruption renames type ItemValueError;
BadValue renames type ItemValueError;
SequenceError renames type SequenceValueError;
SubtleValueError renames type UndetectableValueError;
BenignValueError renames type DetectableValueError;
SubtleValueCorruption renames type DetectableValueError;
-- Detectability (Benign/Subtle) represent a characteristic of error types
--replication errors
ReplicationError: type;
AsymmetricReplicatesError: type extends ReplicationError;
AsymmetricValue: type extends AsymmetricReplicatesError;
AsymmetricApproximateValue: type extends AsymmetricValue;
AsymmetricExactValue: type extends AsymmetricValue;
AsymmetricTiming: type extends AsymmetricReplicatesError;
AsymmetricOmission: type extends AsymmetricReplicatesError;
AsymmetricItemOmission: type extends AsymmetricOmission;
AsymmetricServiceOmission: type extends AsymmetricOmission;
SymmetricReplicatesError: type extends ReplicationError;
SymmetricValue: type extends SymmetricReplicatesError;
SymmetricApproximateValue: type extends SymmetricValue;
SymmetricExactValue: type extends SymmetricValue;
SymmetricTiming: type extends SymmetricReplicatesError;
SymmetricOmission: type extends SymmetricReplicatesError;
SymmetricItemOmission: type extends SymmetricOmission;
SymmetricServiceOmission: type extends SymmetricOmission;
-- aliases for replication
InconsistentValue renames type AsymmetricValue;
InconsistentTiming renames type AsymmetricTiming;
InconsistentOmission renames type AsymmetricOmission;
InconsistentItemOmission renames type AsymmetricItemOmission;
InconsistentServiceOmission renames type AsymmetricServiceOmission;
AsymmetricTransmissive renames type AsymmetricValue;
--concurrency errors
ConcurrencyError: type;
RaceCondition: type extends ConcurrencyError;
ReadWriteRace: type extends RaceCondition;
WriteWriteRace: type extends RaceCondition;
MutExError: type extends ConcurrencyError;
Deadlock: type extends MutExError;
Starvation: type extends MutExError;
--authorization and authentication errors
AuthorizationError: type;
AuthenticationError: type;
end types;
**};
end ErrorLibrary;
resources/AADLv2/replication_properties.aadl 0 → 100644
View file @ b26ec36a
property set Replication_Properties is
-- description of the context, requirements and goal of the replication
Description : aadlstring applies to (system, process, thread, processor, device);
-- Specification of the replica number
Replica_Number : aadlinteger applies to ( system, process, thread, processor, device);
-- Min_Nbr_Replica: A constant that represents the minimal number of replica.
Min_Nbr_Replica : constant aadlinteger => 3 ;
-- Max_Nbr_Replica: A constant that represents the maximal number of replica.
Max_Nbr_Replica : constant aadlinteger => 7 ;
-- Identifiers of the different generated replica
Replica_Identifiers : list of aadlstring applies to (system, process, thread, processor, device);
--Replication type
-- Passive Replication: one replica has two behaviors (primary and backup behaviors)
-- Active Replication: all replica have the same behavior and there is a consensus algorithm to vote between them
Replication_Types: type enumeration (ACTIVE , PASSIVE);
Replica_Type : Replication_Properties::Replication_Types applies to (system, process, thread, processor, device);
-- the consensus algorithm source text
Consensus_Algorithm_Source_Text: aadlString applies to (port, data access, system, processor, device);
-- to refer to a subprogram or thread classifier
Consensus_Algorithm_Class : classifier (subprogram) applies to (port, data access, system, processor, device);
-- to refera subprogram or a thread instance
Consensus_Algorithm_Ref : reference (subprogram) applies to (port, data access, system, processor, device);
end Replication_Properties;
resources/Makefile.am
View file @ b26ec36a
......@@ -28,6 +28,8 @@ AADL_V2_PROPERTIES = $(srcdir)/AADLv2/aadl_project.aadl \
$(srcdir)/AADLv2/pok_properties.aadl \
$(srcdir)/AADLv2/programming_properties.aadl \
$(srcdir)/AADLv2/base_types.aadl \
$(srcdir)/AADLv2/replication_properties.aadl \
$(srcdir)/AADLv2/errorlibrary.aadl \
$(srcdir)/AADLv2/taste_properties.aadl \
$(srcdir)/AADLv2/transformations.aadl
......
resources/ocarina_config.aadl
View file @ b26ec36a
......@@ -62,4 +62,18 @@ property set Ocarina_Config is
Timeout_Property : Time applies to (system);
-- The timeout used to stop an execution
Annex_Type : type enumeration
(annex_all,
annex_none,
behavior_specification,
real_specification,
emv2);
-- Designates the list of annexes supported in ocarina. annex_all
-- and annex_none designate respectively all supported annexes
-- and none of them for properties that accept this kind of
-- designation.
Enable_Annexes : list of Ocarina_Config::Annex_Type applies to (system);
-- List of annexes to be enabled in the parsed model
end Ocarina_Config;
src/backends/ocarina-backends-expander.adb
View file @ b26ec36a
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2015 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2016 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -193,11 +193,11 @@ package body Ocarina.Backends.Expander is
end if;
Append_Node_To_List
(Make_Node_Container (L),
(Make_Node_Container (L, Extra_Item (K)),
Sources (N));
Append_Node_To_List
(Make_Node_Container (N),
(Make_Node_Container (N, Extra_Item (K)),
Destinations (L));
end if;
......@@ -227,11 +227,11 @@ package body Ocarina.Backends.Expander is
end if;
Append_Node_To_List
(Make_Node_Container (L),
(Make_Node_Container (L, Extra_Item (K)),
Destinations (N));
Append_Node_To_List
(Make_Node_Container (N),
(Make_Node_Container (N, Extra_Item (K)),
Sources (L));
end if;
......
src/backends/ocarina-backends-lnt-components.adb 0 → 100644
View file @ b26ec36a
This diff is collapsed.
src/backends/ocarina-backends-lnt-components.ads 0 → 100644
View file @ b26ec36a
------------------------------------------------------------------------------
-- --
-- OCARINA COMPONENTS --
-- --
-- O C A R I N A . B A C K E N D S . L N T . C O M P O N E N T S --
-- --
-- S p e c --
-- --
-- Copyright (C) 2016 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. Ocarina is distributed in the hope that it will be useful, but --
-- WITHOUT ANY WARRANTY; without even the implied warranty of --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --