package with_foundation
public

with Base_Types;

system sys
end sys;

system implementation sys.impl
subcomponents
	thr: thread thr.impl;
end sys.impl;

thread thr
features
	p1: in event data port {
		Input_Time => ([time => Dispatch; offset => 0 ms;]);
	};
	p2: in event data port; -- has default Input_Time as below

	q1: in event data port {
		Input_Time => (
			[time => Dispatch; offset => 0 ms;],
			[time => Start; offset => 5 ms;]);
	};
	q2: in event data port {
		Input_Time => (
			[time => Dispatch; offset => 0 ms;],
			[time => Start; offset => 5 ms;]);
	};

	z: in event data port {
		Input_Time => (
			[time => Start; offset => 5 ms;]);
	};
end thr;

thread implementation thr.impl
subcomponents
	a: data Base_Types::Integer;
annex behavior_specification {**states
	s: initial complete final state;
	s1: state;
transitions
	-- The following two transition definitions are absolutely the same
	-- This makes useless the 'frozen' keyword until some changes are done.
	s -[on dispatch p1 frozen p2]-> s1 {
		-- As for 8.3.2(21), p1, p2, q1, q2 will be frozen.
		a := 1
	};
	s -[on dispatch p1]-> s1 {
		-- As for 8.3.2(21), p1, p2, q1, q2 will be frozen.
		a := 1
	};

	s -[on dispatch q1 frozen q2]-> s1 {
		-- As for 8.3.2(21), p1, p2, q1, q2 will be frozen.
		a := 2
	};
	s -[on dispatch p1 frozen z]-> s1 {
		-- Contradicts with 8.3.2(18).
		a := 3
	};
	s -[on dispatch p1]-> s1 {
		z<<; -- Contradicts with D.5(7) and 8.3.2(18).
		a := 3
	};
**};end thr.impl;

end with_foundation;