I get a bug during "Generate Minimal Cut Sets"

[yiji-kong]

but, I get the reaults, there is nothing:

The aadl looks like:

package Integer_Toy
public
with Base_Types;
with faults;

system A
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
	assume "A input range" : Input < 20;
	guarantee "A output range" : Output < 2*Input;
**};	

annex safety {**
	fault stuck_at_fault_A "Component A output stuck" : faults::fail_to {
		inputs: val_in <- Output, alt_val <- prev(Output, 0); 
		outputs: Output <- val_out;    
    	probability: 5.0E-9 ;
		duration: permanent;
	}
**};

end A ;

system B
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
	assume "B input range" : Input < 20;
	guarantee "B output range" : Output < Input + 15;
**};

annex safety {**
	fault stuck_at_fault_B "Component B output stuck nondeterministic" : faults::fail_to {
		eq nondet_val : int;
		inputs: val_in <- Output, alt_val <- nondet_val; 
		outputs: Output <- val_out;    
    	probability: 5.0E-5 ;
		duration: permanent;
	}
**};	

end B ;

system C
features
Input1: in data port Base_Types::Integer;
Input2: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
  eq mode : int;
  
  guarantee "mode always is increasing" : mode >= 0 -> mode > pre(mode);
	guarantee "C output range" : Output = if mode = 3 then (Input1 + Input2) else 0;
**};	

end C ;

system top_level
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;
annex agree {**

  eq mode : int;
	assume "System input range " : Input < 10;
	guarantee "mode is always positive" : mode >= 0;
	guarantee "System output range" : Output < 50;
**};	

end top_level;

system implementation top_level.Impl
subcomponents
A_sub : system A ;
B_sub : system B ;
C_sub : system C ;
connections
IN_TO_A : port Input -> A_sub.Input {Communication_Properties::Timing => immediate;};
A_TO_B : port A_sub.Output -> B_sub.Input {Communication_Properties::Timing => immediate;};
A_TO_C : port A_sub.Output -> C_sub.Input1 {Communication_Properties::Timing => immediate;};
B_TO_C : port B_sub.Output -> C_sub.Input2 {Communication_Properties::Timing => immediate;};
C_TO_Output : port C_sub.Output -> Output {Communication_Properties::Timing => immediate;};

annex agree{**
  assign mode = C_sub.mode;
**};

annex safety{**
  --analyze : probability 1.0E-7
  analyze : max 2 fault

**};
end top_level.Impl;

end Integer_Toy;

[dkstewart]

Hi yiji-kong, I am trying to re-create this problem to no avail. Can you provide a bit more information for me? Are there any exceptions being thrown? Are all properties being verified correctly when the analysis proceeds? One thing you could try is cleaning the project in the workspace (click on menu item Project -> Clean...) and then re-running the analysis.

[zhangzelun125]

Hi yiji-kong, I am trying to re-create this problem to no avail. Can you provide a bit more information for me? Are there any exceptions being thrown? Are all properties being verified correctly when the analysis proceeds? One thing you could try is cleaning the project in the workspace (click on menu item Project -> Clean...) and then re-running the analysis.

Excuse me,I have got the same bug when I try to use the function "Generate Minimal Cut Sets"; I can just use it correctly tow months ago;The OSATE version is 2.7.3,and the Safety Annex version is 1.0.0.201909271336

When I try to Ggenerate minimal cut sets,the console will give the waring,an the example I use is the Integer_Toy given by your newest ASAME‘example：

And the counterexample is:

When I try to change the SMT Solver from SMTInterpol to Z3,the result is:

Would you please help me?I have tried to clean the project but it didn't work.

[dkstewart]

A likely cause is the version of Osate you are using and the older version of the safety annex you have installed. Agree/Amase (safety annex) have been tested and released for Osate 2.7.0. When I run this version of Osate with the most recent safety annex release, these problems do not show up.

Here is a link to install instructions and the version numbers appropriate. If you install Osate 2.7.0 and go through these instructions, it should solve the problem. Let me know if there are any problems you encounter. https://github.com/loonwerks/AMASE/tree/master/safety-update-site

[zhangzelun125]

A likely cause is the version of Osate you are using and the older version of the safety annex you have installed. Agree/Amase (safety annex) have been tested and released for Osate 2.7.0. When I run this version of Osate with the most recent safety annex release, these problems do not show up.

Here is a link to install instructions and the version numbers appropriate. If you install Osate 2.7.0 and go through these instructions, it should solve the problem. Let me know if there are any problems you encounter. https://github.com/loonwerks/AMASE/tree/master/safety-update-site

In the update site field, enter the following website: https://raw.githubusercontent.com/loonwerks/AMASE/master/safety-update-site/safety-annex_0.9，but I get an error:

becaues the site cannot be visited:

The browser is Chrome.Would you please guide me?Thank you.

[dkstewart]

It makes sense that you cannot visit the site on Chrome - it is an update site used for the install. That being said, it should be able to find the software through Osate install.

Using Osate 2.7.0, go to menu item: Help -> Install new software... then in the "Work with" field, but in that website. When I perform these actions on Windows 10 or Mac OS x 10.12, this is what shows up:

What version of Osate are you using? And what operating system? These might help me narrow down your problem.

[zhangzelun125]

The version of Osate is 2.7.0, and the opeating system is Windows 10,I still cannot find software on the website:

[yiji-kong]

Sorry to bother again. I tried another time, but I still got nothing about the “Generate Minimal Cut Sets”；
My Osate ：2.7.0 for win10

And I installed the plugin successfully.

And the environment variable called “MHS_HOME”:

The PATH:

The AADL:
1.faults：
package faults
public
annex agree {**

node fail_to(val_in: int, alt_val: int, trigger: bool) returns (val_out: int); 
let
   val_out = if (trigger) then alt_val else val_in;
tel;

node inverted_fail(val_in: bool, trigger: bool) returns (val_out:bool);
let
  val_out = if trigger then not(val_in) else val_in;
tel;

node no_data_fail(val_in : bool, trigger: bool) returns (val_out: bool);
let
	val_out = if trigger then (val_in) else not(val_in);
tel;

node fail_to_bool(val_in: bool, alt_val: bool, trigger: bool) returns (val_out: bool); 
let
   val_out = if (trigger) then alt_val else val_in;
tel;

**};

end faults;

2.Integer_Toy：
package Integer_Toy
public
with Base_Types;
with faults;

system A
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
	assume "A input range" : Input < 20;
	guarantee "A output range" : Output < 2*Input;
**};	

annex safety {**
	fault stuck_at_fault_A "Component A output stuck" : faults::fail_to {
		inputs: val_in <- Output, alt_val <- prev(Output, 0); 
		outputs: Output <- val_out;    
    	probability: 5.0E-9 ;
		duration: permanent;
	}
**};

end A ;

system B
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
	assume "B input range" : Input < 20;
	guarantee "B output range" : Output < Input + 15;
**};

annex safety {**
	fault stuck_at_fault_B "Component B output stuck nondeterministic" : faults::fail_to {
		eq nondet_val : int;
		inputs: val_in <- Output, alt_val <- nondet_val; 
		outputs: Output <- val_out;    
    	probability: 5.0E-5 ;
		duration: permanent;
	}
**};	

end B ;

system C
features
Input1: in data port Base_Types::Integer;
Input2: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;

annex agree {** 
  eq mode : int;
  
  guarantee "mode always is increasing" : mode >= 0 -> mode > pre(mode);
	guarantee "C output range" : Output = if mode = 3 then (Input1 + Input2) else 0;
**};	

end C ;

system top_level
features
Input: in data port Base_Types::Integer;
Output: out data port Base_Types::Integer;
annex agree {**

  eq mode : int;
	assume "System input range " : Input < 10;
	guarantee "mode is always positive" : mode >= 0;
	guarantee "System output range" : Output < 50;
**};	

end top_level;

system implementation top_level.Impl
subcomponents
A_sub : system A ;
B_sub : system B ;
C_sub : system C ;
connections
IN_TO_A : port Input -> A_sub.Input {Communication_Properties::Timing => immediate;};
A_TO_B : port A_sub.Output -> B_sub.Input {Communication_Properties::Timing => immediate;};
A_TO_C : port A_sub.Output -> C_sub.Input1 {Communication_Properties::Timing => immediate;};
B_TO_C : port B_sub.Output -> C_sub.Input2 {Communication_Properties::Timing => immediate;};
C_TO_Output : port C_sub.Output -> Output {Communication_Properties::Timing => immediate;};

annex agree{**
  assign mode = C_sub.mode;
**};

annex safety{**
  --analyze : probability 1.0E-7
  analyze : max 2 fault

**};
end top_level.Impl;

end Integer_Toy;

I selected the “system implementation top_level.Impl” in “Integer_Toy”；

And still nothing.

[dkstewart]

Only select "Safety Annex" for the installation, and not "Safety Annex Source Code." This might be the problem.

Do not reinstall Osate, but instead click on Help -> About Osate 2 -> Installation details
then select Safety Annex Source Code -> Uninstall. See if that works. If not, please let me know.

I also assume that since MHS_HOME is set, you downloaded the source executable for the MHS algorithm onto your local machine. If not, certainly do that. (Step 1 of the install instructions.)