Commit 2956fa8c authored by Bechir Zalila's avatar Bechir Zalila

* Test cases for the bahaviour annexe front end

	(By Yossra Rekik)
parent 6d33cabb
......@@ -275,6 +275,33 @@ examples/real/security/all.aadl
examples/real/resources/all.aadl
#examples/real/safety/model.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_sub_1.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_sub_2.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_sub_3.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_th_1.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_th_2.aadl
tests/test_behavior_annex/test_ba_parser/ba_example_th_3.aadl
tests/test_behavior_annex/test_ba_analyzer/test1.aadl
tests/test_behavior_annex/test_ba_analyzer/test2.aadl
tests/test_behavior_annex/test_ba_analyzer/test3.aadl
tests/test_behavior_annex/test_ba_analyzer/test4.aadl
tests/test_behavior_annex/test_ba_analyzer/test5.aadl
tests/test_behavior_annex/test_ba_analyzer/test6.aadl
tests/test_behavior_annex/test_ba_analyzer/test7.aadl
tests/test_behavior_annex/test_ba_analyzer/test8.aadl
tests/test_behavior_annex/test_ba_analyzer/test9.aadl
tests/test_behavior_annex/test_ba_analyzer/test10.aadl
tests/test_behavior_annex/test_ba_analyzer/test11.aadl
tests/test_behavior_annex/test_ba_analyzer/test12.aadl
tests/test_behavior_annex/test_ba_analyzer/test13.aadl
tests/test_behavior_annex/test_ba_analyzer/test14.aadl
tests/test_behavior_annex/test_ba_analyzer/test15.aadl
tests/test_behavior_annex/test_ba_analyzer/test16.aadl
tests/test_behavior_annex/test_ba_analyzer/test17.aadl
tests/test_behavior_annex/test_ba_analyzer/test18.aadl
tests/test_behavior_annex/test_ba_analyzer/test19.aadl
tests/test_behavior_annex/test_ba_analyzer/test20.aadl
tests/test_identifier/t.aadl
tests/example_04_03/t.aadl
tests/example_04_05_1/t.aadl
......
AADL_VERSION=-aadlv2
OCARINA_FLAGS=-p data_model.aadl base_types.aadl
package exemple1
public
with Base_Types ;
subprogram sub
end sub;
subprogram implementation sub.good
annex behavior_specification {**
states
uniqueState : initial final state ;
**};
end sub.good;
subprogram implementation sub.error1
annex behavior_specification {**
-- Errors: The behavior annex of a subprogram
-- _ can't have more than one initial state.
-- _ must define one final state.
-- _ can't have complete state.
states
initState1 : initial state ;
initState2 : initial state ;
compState : complete state ;
**};
end sub.error1;
subprogram implementation sub.error2
annex behavior_specification {**
-- Errors: The behavior annex of a subprogram
-- _ can't have more than one final state.
states
uniqueState : initial final state ;
finalState1 : final state ;
**};
end sub.error2 ;
end exemple1 ;
test1.aadl:30:02: sub.error1 ( Subprogram ) can't have more than one initial state.
test1.aadl:31:02: sub.error1 ( Subprogram ) can't have complete state.
test1.aadl:28:01: sub.error1 ( Subprogram ) has no final state.
Cannot analyze BEHAVIOR_SPECIFICATION specifications
-- This example gives a basic implementation of a stack data type associated
-- with its access methods. The various corresponding AADL component
-- specifications are encompassed within a same package to offer an Object-
-- Oriented Class style.
package BA_example2 public
with Base_Types;
data stack
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 {**
-- Errors : Local variables must be explicitly typed
-- with a valid data component classifier
-- (pop) is not of type Data.
variables
t : pop;
states
s0 : initial final state;
**};
end push.default;
end BA_example2;
test10.aadl:41:11: (pop) does not point to anything or to something unreachable.
test10.aadl:41:07: behavior variable(s) must be explicitly typed with a valid data component classifier.
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package exemple
public
with Base_Types ;
subprogram sub
end sub;
subprogram implementation sub.error
annex behavior_specification {**
states
uniqueState : initial final state ;
-- Errors :
-- ** Subprogram can't have dispatch condition in any of its transitions.
transitions
uniqueState -[on dispatch]-> uniqueState ;
**};
end sub.error ;
end exemple ;
test11.aadl:21:02: Subprogram components must not contain a dispatch condition in any of its transitions
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package exemple
public
with Base_Types ;
thread th
end th;
thread implementation th.good
annex behavior_specification {**
states
uniqueState : initial complete final state ;
transitions
uniqueState -[on dispatch]-> uniqueState ;
**};
end th.good;
thread implementation th.error
annex behavior_specification {**
states
compState : initial complete state ;
exeState : state ;
finalState : final state ;
transitions
-- Errors:
-- ** transitions out of complete states must have dispatch conditions.
compState -[]-> finalState ;
**};
end th.error;
end exemple ;
test12.aadl:35:03: "compState" Transitions out of complete states must have dispatch condition
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package exemple
public
with Base_Types ;
thread th
end th;
thread implementation th.good
annex behavior_specification {**
states
uniqueState : initial complete final state ;
transitions
uniqueState -[on dispatch]-> uniqueState ;
**};
end th.good;
thread implementation th.error
annex behavior_specification {**
states
compState : initial complete state ;
exeState : state ;
finalState : final state ;
transitions
-- Errors :
-- ** transitions states that are final only are not allowed.
-- ** only transitions out of complete states may have dispatch conditions.
finalState -[on dispatch]-> finalState ;
**};
end th.error;
end exemple ;
test13.aadl:37:03: "finalState" Transitions out of final states are not allowed
test13.aadl:37:03: "finalState" Only transition out of complete states may have dispatch condition
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package example1 public
with Base_Types;
subprogram addition
features
x: in parameter Base_Types::Integer;
y: in parameter Base_Types::Integer;
r: out parameter Base_Types::Integer;
ovf: out parameter Base_Types::Boolean;
end addition;
subprogram implementation addition.default
annex behavior_specification {**
states
s0 : initial state;
s1 : final state;
transitions
regular: s2 -[ ]-> s3 { r := x + y ; ovf := false };
overflow: s0 -[ ]-> s1 { r := 0; ovf := true };
**};
end addition.default;
end example1;
test14.aadl:19:14: "s2" is not found in States
test14.aadl:19:24: "s3" is not found in States
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch p ]-> next2 { x1 := p1 };
-- errors :
-- "p" (dispatch trigger) does not point to any event port or subprogram access feature
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test15.aadl:20:23: "p" (dispatch trigger) does not point to any event port or subprogram access feature
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch m ]-> next2 { x1 := p1 }; -- errors : "m" (dispatch trigger) must refer to an IN event port or IN event data port
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test16.aadl:20:23: "m" (dispatch trigger) must refer to an IN event port or IN event data port
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
data d
end d;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
r : requires data access d;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch r ]-> next2 { x1 := p1 }; -- errors : "r" (dispatch trigger) must refer to a provides subprogram access feature
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test17.aadl:23:23: "r" (dispatch trigger) must refer to a provides subprogram access feature
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
k : in data port Base_Types::Integer;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch k ]-> next2 { x1 := p1 }; -- errors : "k" (dispatch trigger) must refer to an IN event port or IN event data port
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test18.aadl:21:23: "k" (dispatch trigger) must refer to an IN event port or IN event data port
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch p1 frozen k ]-> next2 { x1 := p1 }; -- errors : "k" (frozen port) does not point to any port
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test19.aadl:20:33: "k" (frozen port) does not point to any port
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package exemple2
public
with Base_Types ;
thread th
end th;
thread implementation th.good
annex behavior_specification {**
states
uniqueState : initial final state ;
finalState1 : final state ;
compState : complete state ;
**};
end th.good;
thread implementation th.error
annex behavior_specification {**
-- Errors: The behavior annex of a thread
-- _ can't have more than one initial state.
-- _ must define one or more final states.
-- _ must define one or more complete states.
states
initState1 : initial state ;
initState2 : initial state ;
**};
end th.error;
end exemple2 ;
test2.aadl:31:02: th.error ( Thread ) can't have more than one initial state.
test2.aadl:29:01: th.error ( Thread ) must define one or more complete states.
test2.aadl:29:01: th.error ( Thread ) must define one or more final states.
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example public
with Base_Types;
thread merger
features
p1 : in event data port Base_Types::Integer;
p2 : in event data port Base_Types::Integer;
m : out event data port Base_Types::Integer;
end merger;
thread implementation merger.impl
annex behavior_specification {**
states
s0 : initial complete state;
comp : state;
next1, next2 : complete final state;
transitions
s0 -[ on dispatch p1 frozen m ]-> next2 { x1 := p1 }; -- errors : "m" (frozen port) must refer to an IN port
s0 -[ on dispatch p2 ]-> next1 { x2 := p2 };
**};
end merger.impl;
end BA_example;
test20.aadl:20:33: "m" (frozen port) must refer to an IN port
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example1 public
with Base_Types;
data stack
end stack;
data implementation stack.default
subcomponents
elems : data Base_Types::Integer [100];
sp : data Base_Types::Integer;
end stack.default;
subprogram addition
features
x: in parameter Base_Types::Integer;
y: in parameter Base_Types::Integer;
r: out parameter Base_Types::Integer;
ovf: out parameter Base_Types::Boolean;
end addition;
subprogram implementation addition.default
annex behavior_specification {**
-- Errors : The variable identifiers must be
-- unique within a behavior annex subclause
variables
v : stack;
s,v : Stack;
**};
end addition.default;
end BA_example1;
test3.aadl:30:05: "v" conflicts with declaration at line 29
Cannot analyze BEHAVIOR_SPECIFICATION specifications
package BA_example1 public
with Base_Types;
data stack
end stack;
data implementation stack.default
subcomponents
elems : data Base_Types::Integer [100];
sp : data Base_Types::Integer;
end stack.default;
subprogram addition
features
x: in parameter Base_Types::Integer;
y: in parameter Base_Types::Integer;
r: out parameter Base_Types::Integer;
ovf: out parameter Base_Types::Boolean;
end addition;
subprogram implementation addition.default
annex behavior_specification {**
-- Errors : The variable identifiers must not
-- conflict with mode identifiers,
-- feature identifiers, or data
-- subcomponent identifiers of the component
-- for which the behavior annex subclause
-- is defined.(Naming rule N1)
variables
v : stack;
s,y : Stack;
**};
end addition.default;
end BA_example1;
test4.aadl:35:05: "y" conflicts with declaration at line 17
package BA_example1 public
with Base_Types;
data stack
end stack;
data implementation stack.default
subcomponents
elems : data Base_Types::Integer [100];
sp : data Base_Types::Integer;
end stack.default;
subprogram addition
features
x: in parameter Base_Types::Integer;
y: in parameter Base_Types::Integer;
r: out parameter Base_Types::Integer;
ovf: out parameter Base_Types::Boolean;
end addition;
subprogram implementation addition.default
annex behavior_specification {**
-- Errors : The state identifiers must be
-- unique within a behavior annex subclause
states
s0 : initial state;
s1,s0 : final state;
**};
end addition.default;
end BA_example1;