Commit 1772abb3 authored by yoogx's avatar yoogx
Browse files

* Defends against incomplete BA specification

        For openaadl/ocarina#189
parent 2d9b6d95
......@@ -927,7 +927,8 @@ package body Ocarina.Analyzer.AADL_BA is
-- In the case of a sequence of behavior actions
if not Is_Empty (BATN.Behavior_Action_Sequence (Behav_actions))
if Present (Behav_Actions) and then
not Is_Empty (BATN.Behavior_Action_Sequence (Behav_actions))
then
Behav_action := BATN.First_Node
......@@ -943,7 +944,8 @@ package body Ocarina.Analyzer.AADL_BA is
-- In the case of a set of behavior actions:
if not Is_Empty (BATN.Behavior_Action_Set (Behav_actions))
if Present (Behav_Actions) and then
not Is_Empty (BATN.Behavior_Action_Set (Behav_actions))
then
Behav_action := BATN.First_Node
(BATN.Behavior_Action_Set (Behav_actions));
......@@ -958,11 +960,10 @@ package body Ocarina.Analyzer.AADL_BA is
-- In the case of a single action
if Present (BATN.Behavior_Action (Behav_actions))
and then
Is_Empty (BATN.Behavior_Action_Sequence (Behav_actions))
and then
Is_Empty (BATN.Behavior_Action_Set (Behav_actions))
if Present (Behav_Actions) and then
Present (BATN.Behavior_Action (Behav_actions)) and then
Is_Empty (BATN.Behavior_Action_Sequence (Behav_actions)) and then
Is_Empty (BATN.Behavior_Action_Set (Behav_actions))
then
Success := Success and then Analyze_Behavior_Action
(BATN.Behavior_Action (Behav_actions),
......
property set Data_Model is
Base_Type : list of classifier (
data)
applies to (data);
Code_Set : aadlinteger
applies to (data);
Data_Digits : aadlinteger
applies to (data);
Data_Scale : aadlinteger
applies to (data);
Data_Representation : enumeration (Array, Boolean, Bounded_Array, Character, Enum, Float, Fixed, Integer, String, Struct, Union)
applies to (data);
Dimension : list of aadlinteger
applies to (data);
Indefinite_Dimension : constant aadlinteger => -1;
Infinite_Dimension : constant aadlinteger => -2;
Element_Names : list of aadlstring
applies to (data);
Enumerators : list of aadlstring
applies to (data);
IEEE754_Precision : enumeration (Simple, Double)
applies to (data);
Initial_Value : list of aadlstring
applies to (data, port, parameter);
Integer_Range : range of aadlinteger
applies to (data, port, parameter);
Measurement_Unit : aadlstring
applies to (data, port, parameter);
Number_Representation : enumeration (Signed, Unsigned)
applies to (data);
Real_Range : range of aadlreal
applies to (data, port, parameter);
Representation : list of aadlstring
applies to (data);
end Data_Model;
package Base_Types
public
with data_model;
data Boolean
properties
Data_Model::Data_Representation => Boolean;
end Boolean;
data Integer
properties
Data_Model::Data_Representation => Integer;
end Integer;
data Integer_8 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 1 Bytes;
end Integer_8;
data Integer_16 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 2 Bytes;
end Integer_16;
data Integer_32 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 4 Bytes;
end Integer_32;
data Integer_64 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 8 Bytes;
end Integer_64;
data Unsigned_8 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 1 Bytes;
end Unsigned_8;
data Unsigned_16 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 2 Bytes;
end Unsigned_16;
data Unsigned_32 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 4 Bytes;
end Unsigned_32;
data Unsigned_64 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 8 Bytes;
end Unsigned_64;
data Natural extends Integer
properties
Data_Model::Integer_Range => 0 .. Max_Target_Integer;
end Natural;
data Float
properties
Data_Model::Data_Representation => Float;
end Float;
data Float_32 extends Float
properties
Data_Model::IEEE754_Precision => Simple;
Source_Data_Size => 4 Bytes;
end Float_32;
data Float_64 extends Float
properties
Data_Model::IEEE754_Precision => Double;
Source_Data_Size => 8 Bytes;
end Float_64;
data Character
properties
Data_Model::Data_Representation => Character;
end Character;
data String
properties
Data_Model::Data_Representation => String;
end String;
end Base_Types;
package BA_example2
public
with Base_Types;
data stack
features
put : provides subprogram access push;
get : provides subprogram access pop;
end stack;
data implementation stack.default
subcomponents
elems : data Base_Types::Integer [100];
sp : data Base_Types::Integer;
end stack.default;
subprogram push
features
this : in out parameter stack.default;
v : in parameter Base_Types::Integer;
overflow : out event port;
end push;
subprogram pop
features
this : in out parameter stack.default;
v : out parameter Base_Types::Integer;
underflow : out event port;
end pop;
subprogram implementation push.default
annex behavior_specification {**
states
s0 : initial state;
s1 : final state;
transitions
s0 -[this. sp >= 100]-> s1 {
this. elems [ this. sp ] := v;
this. sp := this. sp + 1
};
s0 -[this. sp > 100]-> s1 {
overflow !
};
**};
end push.default;
subprogram implementation pop.default
annex behavior_specification {**
states
s0 : initial state;
s1 : final state;
transitions
s0 -[this. sp > 0]-> s1 {
this. sp := this. sp - 1;
v := this. elems [ this. sp ]
};
s0 -[this. sp = 0]-> s1 {
underflow !
};
**};
end pop.default;
end BA_example2;
ba_example_sub_2.aadl:43:36: (overflow) does not point to any subprogram in the AADL model.
Cannot analyze BEHAVIOR_SPECIFICATION specifications
property set Data_Model is
Base_Type : list of classifier (
data)
applies to (data);
Code_Set : aadlinteger
applies to (data);
Data_Digits : aadlinteger
applies to (data);
Data_Scale : aadlinteger
applies to (data);
Data_Representation : enumeration (Array, Boolean, Bounded_Array, Character, Enum, Float, Fixed, Integer, String, Struct, Union)
applies to (data);
Dimension : list of aadlinteger
applies to (data);
Indefinite_Dimension : constant aadlinteger => -1;
Infinite_Dimension : constant aadlinteger => -2;
Element_Names : list of aadlstring
applies to (data);
Enumerators : list of aadlstring
applies to (data);
IEEE754_Precision : enumeration (Simple, Double)
applies to (data);
Initial_Value : list of aadlstring
applies to (data, port, parameter);
Integer_Range : range of aadlinteger
applies to (data, port, parameter);
Measurement_Unit : aadlstring
applies to (data, port, parameter);
Number_Representation : enumeration (Signed, Unsigned)
applies to (data);
Real_Range : range of aadlreal
applies to (data, port, parameter);
Representation : list of aadlstring
applies to (data);
end Data_Model;
package Base_Types
public
with data_model;
data Boolean
properties
Data_Model::Data_Representation => Boolean;
end Boolean;
data Integer
properties
Data_Model::Data_Representation => Integer;
end Integer;
data Integer_8 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 1 Bytes;
end Integer_8;
data Integer_16 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 2 Bytes;
end Integer_16;
data Integer_32 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 4 Bytes;
end Integer_32;
data Integer_64 extends Integer
properties
Data_Model::Number_Representation => Signed;
Source_Data_Size => 8 Bytes;
end Integer_64;
data Unsigned_8 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 1 Bytes;
end Unsigned_8;
data Unsigned_16 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 2 Bytes;
end Unsigned_16;
data Unsigned_32 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 4 Bytes;
end Unsigned_32;
data Unsigned_64 extends Integer
properties
Data_Model::Number_Representation => Unsigned;
Source_Data_Size => 8 Bytes;
end Unsigned_64;
data Natural extends Integer
properties
Data_Model::Integer_Range => 0 .. Max_Target_Integer;
end Natural;
data Float
properties
Data_Model::Data_Representation => Float;
end Float;
data Float_32 extends Float
properties
Data_Model::IEEE754_Precision => Simple;
Source_Data_Size => 4 Bytes;
end Float_32;
data Float_64 extends Float
properties
Data_Model::IEEE754_Precision => Double;
Source_Data_Size => 8 Bytes;
end Float_64;
data Character
properties
Data_Model::Data_Representation => Character;
end Character;
data String
properties
Data_Model::Data_Representation => String;
end String;
end Base_Types;
package BA_example1
public
with Base_types, Data_Model;
thread sender
features
d : out event data port Base_Types::Integer;
a : in event data port Base_Types::Integer;
properties
Dispatch_Protocol => Timed;
Period => 10 Ms;
end sender;
thread implementation sender.v1
subcomponents
v : data Base_Types::Integer;
annex behavior_specification {**
states
st : initial complete state;
sf : complete final state;
s1, s2 : state;
transitions
st -[on dispatch timeout]-> st {
v := 1;
d !(v)
};
st -[on dispatch a]-> s1;
s1 -[a = 1]-> sf;
s1 -[a = 0]-> st;
sf -[on dispatch timeout]-> sf {
v := 0;
d !(v)
};
sf -[on dispatch a]-> s2;
s2 -[a = 0]-> st;
s2 -[a = 1]-> sf;
**};
end sender.v1;
thread implementation sender.v2
annex behavior_specification {**
states
st : initial complete state;
sf : complete final state;
s1, s2 : state;
transitions
st -[on dispatch timeout]-> st {
d !(1)
};
st -[on dispatch a]-> s1;
s1 -[a = 1]-> sf;
s1 -[a = 0]-> st;
sf -[on dispatch timeout]-> sf {
d !(0)
};
sf -[on dispatch a]-> s2;
s2 -[a = 0]-> st;
s2 -[a = 1]-> sf;
**};
end sender.v2;
end BA_example1;
ba_example_th_1.aadl:27:39: (v) does not point to any variable of the current BA or a parameter or a required data access feature of the subprogram having the current BA.
ba_example_th_1.aadl:27:47: (d) does not point to any subprogram in the AADL model.
Cannot analyze BEHAVIOR_SPECIFICATION specifications
property set Data_Model is
Base_Type : list of classifier (
data)
applies to (data);
Code_Set : aadlinteger
applies to (data);
Data_Digits : aadlinteger
applies to (data);
Data_Scale : aadlinteger
applies to (data);
Data_Representation : enumeration (Array, Boolean, Bounded_Array, Character, Enum, Float, Fixed, Integer, String, Struct, Union)
applies to (data);
Dimension : list of aadlinteger
applies to (data);
Indefinite_Dimension : constant aadlinteger => -1;
Infinite_Dimension : constant aadlinteger => -2;
Element_Names : list of aadlstring
applies to (data);
Enumerators : list of aadlstring
applies to (data);
IEEE754_Precision : enumeration (Simple, Double)
applies to (data);
Initial_Value : list of aadlstring
applies to (data, port, parameter);
Integer_Range : range of aadlinteger
applies to (data, port, parameter);
Measurement_Unit : aadlstring
applies to (data, port, parameter);
Number_Representation : enumeration (Signed, Unsigned)
applies to (data);
Real_Range : range of aadlreal
applies to (data, port, parameter);
Representation : list of aadlstring
applies to (data);
end Data_Model;
package Base_Types
public
with data_model;
data Boolean
properties
Data_Model::Data_Representation => Boolean;
end Boolean;
data Integer
properties
Data_Model::Data_Representation => Integer;
end Integer;
data Integer_8 extends Integer
properties