Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Validation of fault_activation reports invalid component name #20

Open
kfhoech opened this issue Nov 29, 2023 · 0 comments
Open

Validation of fault_activation reports invalid component name #20

kfhoech opened this issue Nov 29, 2023 · 0 comments
Labels

Comments

@kfhoech
Copy link
Contributor

kfhoech commented Nov 29, 2023

Validation of "fault_activation" constructs in the safety annex reports error message of form "The fault component: <subcomponent_id> is not a valid component name for the fault: <fault_id>" where the subcomponent type is an abstract component. Fault activation of such form should be allowed (not an error). It is likely that this error message is due to merely to an over-zealous validator.

A simple, self-contained example as as follows:

package Example
public
	with Base_Types;

	abstract Inner
		features
			input1 : in data port Base_Types::Boolean;
			output1 : out data port Base_Types::Boolean;
		annex agree {**
			guarantee Inner_O1 "Inner Output Follows Input" :
				output1 = input1;
			node stuck_false (in1 : bool, trigger : bool) returns (out1 : bool);
			let
				out1 = if trigger then false else in1;
			tel;
		**};
		annex safety {**
			fault Inner_Output_Stuck_False "Inner component output1 is stuck false" : stuck_false {
				inputs: in1 <- output1;
				outputs: output1 <- out1;
				disable: false;
				probability: 1.0e-10;
				duration: permanent;
			}
		**};
	end Inner;

	system Outer
		features
			input1 : in data port Base_Types::Boolean;
			output1 : out data port Base_Types::Boolean;
		annex agree {**
			guarantee Outer_O1 "Outer Output Follows Input" :
				output1 = input1;
		**};
	end Outer;

	system implementation Outer.impl
		subcomponents
			inner : abstract Inner;
		connections
			c_in1 : port input1 -> inner.input1;
			c_out1 : port inner.output1 -> output1;
		annex agree {**
			eq inner_failed : bool;
		**};
		annex safety {**
			fault_activation: inner_failed = Inner_Output_Stuck_False@inner;
			analyze: max 2 fault 
		**};
	end Outer.impl;

end Example;
@kfhoech kfhoech added the bug label Nov 29, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant