Suggestions

[baobao1225]

hi，recently, we've been using your tools FRET, and we have some problems writing requirements,therefore we'd like to offer you some suggestions for improvement.
1.As for scope,sometimes we need to use the operation of the corresponding mode，such as when we want to describe a res happen in the intersection of mode1 and mode2 in FRET，we want to describe in FRET: in mode1&mode2 the system shall satisfy res.but in mode1&mode2 is a Syntax violation.
2.As for timing,sometimes we need a variable that represents a time constant.such as in mode1 the system shall for time1 satisfy res.Time1 is a variable.However,time1 is a Syntax violation.
3.As for simulation,sometimes we need to simulate two or more requirement.Such as requirement1:when signal1 the system shall always sastisfy res . Requirement2:when signal2 the system shall immediately satisfy res. We want to simulate the traces of signal1,signal2,res and two requirement.

Thank you for providing such excellent software.

[anmavrid]

Hello @baobao1225,

Thank you for using FRET and thanks for the suggestions.

Regarding suggestion 1: The FRET grammar allows you to express a boolean expression between two modes if you use the keyword while. So, you could rewrite your example as follows: "while mode1 & mode2 the system shall satisfy res"

I see what you mean in suggestion 2. Thanks!

Regarding suggestion 3: we are already working on extending LTLSIM (the FRET simulator) to support simulation of multiple requirements. We will let you know when we make this publicly available. We are happy that this is a feature that you want to use.

Thank you,
Anastasia

[baobao1225]

Thank for your answer!
Hello,we've been using your tools FRET, and we have a question about FRET.We used the realizability check in your FRET and are curious to achieve the requirements divided into multiple components.We call requirement A Depends on the requiremnet B when the input of A is the output of B.For example,requirement A is (when signal2 the system shall satisfy res) and requirement B is (when signal1 the system shall after 1 seconds satisfy signal2).The output of B is signal2 and the input of A is signal1.Then we can get the dependency analysis of the requirements.

What we want to know is whether there is relevant code in the realizability check that implements the dependency analysis.

Thanks!

[andreaskatis]

Hello,

If I understand this correctly, you are trying to take advantage of the "Compositional" option in realizability checking. The option becomes available only when the original set of requirements for the selected system component can be split into disjoint subsets of requirements, where realizability checking can be performed independently on each subset, instead of the original set (the latter is performed when the "Monolithic" option is enabled in the "Realizability" tab of the "Analysis Portal").

Decomposition for the purposes of realizability checking can only be achieved under specific conditions. The way we currently decompose specifications in FRET, is by computing a set of connected components (CC), where each CC contains requirements that only talk about a subset of the original set of output variables. These output variable subsets are disjoint between CCs.

For example, consider the following two requirements

• R1 : The component shall always satisfy x > 0
• R2 : When z the component shall always satisfy y <= 50

In the above example, if z is a system input, and x and y are system outputs (i.e., you have declared each of them as "Output" in "Variable Mapping"), then requirements R1 and R2 can be independently checked for realizability, and the result would be equivalent to checking realizability of R1 /\ R2.

For more information on how the above is achieved, you can check out our technical report here. We also have a paper that we will be presenting at Formal Methods 2021 in November.

Now, regarding your example involving requirements A and B, we are missing some information regarding the types of variables signal1, signal2 and res . Are they system inputs , outputs, or something else?

[baobao1225]

Thank you very much.signal1 and signal2 are inputs, and res is outputs,I will read the technical report,Thank for your answer.

[SoftPro]

Hello，I'm a student. I'm interested in the path generation template in FRET, but I haven't found it for a long time. Can you provide it? Finally, thank you very much for providing such good software as fret.

[anmavrid]

I am closing this issue. I replied to SoftPro in a separate issue.