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

Bug: Realizability analysis not working #31

Open
jendavis opened this issue Jan 6, 2020 · 0 comments
Open

Bug: Realizability analysis not working #31

jendavis opened this issue Jan 6, 2020 · 0 comments

Comments

@jendavis
Copy link
Contributor

jendavis commented Jan 6, 2020

I found that realizability analysis was working in the October 10 version of the nightly fmw build but not in the November 18 version. I believe this is still an issue with the current build. I pasted the plaintext for a small model that exhibits this issue when running realizability analysis on top_level (a system) as well as the error message I received.

image (1)


package Adder
public
with Base_Types;

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

annex agree {** 
	guarantee "B output range" : Output = 1;
**};	

end B ;

system C
features
Output: out data port Base_Types::Integer;

annex agree {** 
	guarantee "C output range" : Output = 4;
**};	

end C ;

system top_level
features
Output: out data port Base_Types::Integer;
annex agree {**
guarantee "System output is sum of component outputs" : Output = B_out + C_out;
guarantee "System output is 5" : Output = 5;
eq B_out : int;
eq C_out : int;
**};
end top_level;

system implementation top_level.Impl
subcomponents
B_sub : system B ;
C_sub : system C ;
annex agree {**
assign B_out = B_sub.Output;
assign C_out = C_sub.Output;
assign Output = B_out + C_out;
**};

end top_level.Impl;

end Adder;

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant