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.
package Adder
public
with Base_Types;
system B
features
Output: out data port Base_Types::Integer;
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;
};
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.
package Adder public with Base_Types;
system B features Output: out data port Base_Types::Integer;
end B ;
system C features Output: out data port Base_Types::Integer;
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;