Description of complex requirements

[nasa-sw-vnv]

Description of complex requirements

[artimid]

Hello, This type of requirement would probably translate into more than one FRETish sentences. Here are some ideas that may work for your case: 1) Capturing the fact that when the compressor turns on, the signal must stay off for 5 seconds (using 5 as an example): When compressor=on, the signal shall for 5 seconds satisfy signal_value=off 2) Capturing the fact that when the compressor turns on, the signal must enter the toggled_state after 5 seconds: When compressor=on, the signal shall after 5 seconds satisfy toggled_state=on 3) Describing the toggled_state mode In toggled mode, if signal_value=off the signal shall at the next timepoint satisfy signal_value=on In toggled mode, if signal_value=on the signal shall at the next timepoint satisfy signal_value=off You would need to associate the toggled mode with the toggled_state variable in the analysis portal. We are actually working on making this easier in a new extension to the FRETish language that we are working on. I would be happy to discuss these further or discuss other ideas you may have for capturing this requirement. Thanks, Dimitra

…

On Wed, Sep 8, 2021 at 9:25 AM baobao1225 ***@***.***> wrote: Hello,Recently, I have been using FRET to describe some of the requirments, and I am facing some difficulties.The simple description is the following.When Compressor is started, the signal needs to stay off for a period of time and then enter the toggled state. The toggled state means that signal turns on and false alternates continuously.We can assume that compressor is the input and signal is the output. I want to ask if there is a description of this requirement.The following picture is the concrete description.The time can be any number. [image: Requirement] <https://user-images.githubusercontent.com/75615490/132547517-395032e5-04cd-45a6-a3ff-80df3b4e0daf.png> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#27>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACGVMKOYVARWN6GXQ3O4QQ3UA6E53ANCNFSM5DVHBALA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[baobao1225]

Thank you,I have another question about the semantic of "when",for the FRET requirement "when signal the system shall immediately satisfy response",assumed that the first tick signal is false,the second tick signal is true,the third tick the signal is true,the response must be true at the third tick?

[artimid]

Hi, "when condition" determines the requirement trigger to occur at the timepoint where the condition becomes true from false. In your example above, the signal becomes true (from false) at the second tick. Since the response must be satisfied immediately, it must be true at the second tick. If you said "at the next timepoint", then response would have to be true at the third tick. I actually recommend that you also look at the diagrams produced by FRET when you press on "semantics" after entering the FRETish requirement. You can also experiment with the simulator and see if what you wrote corresponds to what you meant. Hope that helps, Dimitra

…

On Wed, Sep 8, 2021 at 9:34 PM baobao1225 ***@***.***> wrote: Thank you,I have another question about the semantic of "when",for the FRET requirement "when signal the system shall immediately satisfy response",assumed that the first tick signal is false,the second tick signal is true,the third tick the signal is true,the response must be true at the third tick? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#27 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACGVMKLQYPFHTZNTXQYJUNTUBA2M5ANCNFSM5DVHBALA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[baobao1225]

Thanks a lot,I used the simulator,but I am confused that the third point REQ is falsed

[artimid]

Ha yes, I understand your confusion! So, the simulator displays two pieces of information: 1) The overall value of the requirement for the example execution. This is the green band that highlights the last row. This means that the requirement is true. 2) The little colored dots at each timepoint. Each dot represents the value of the requirement if the execution were to start at that point.The value/color of 1) is basically the color of dot at time 0 (this is when you display the future-time formula). Now the reason that the dot at time 3 is red is that, if we were to interpret the requirement starting at point 3 (so imagine time started at that point), the signal is true, but the response is false. Note that conditions also trigger the requirement when the conditions are true in the initial state of the scope interval, in this case timepoint 3. Do you see what I mean? I will be happy to explain differently if this is unclear.

…

On Wed, Sep 8, 2021 at 9:54 PM baobao1225 ***@***.***> wrote: Thanks a lot,I used the simulator,but I am confused that the third point REQ is falsed [image: image] <https://user-images.githubusercontent.com/75615490/132624804-629a5528-fef7-488a-8c5e-739e392ae707.png> — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#27 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACGVMKMMLCWWBMEDLU6JPSTUBA4YFANCNFSM5DVHBALA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[baobao1225]

Thank you a lot,I understand your meaning,I am happy to talk with you.

[baobao1225]

hello,I check the requirments,but I am confused about the result.In my opinion,The requirments describes the toggled behavior,but there is a FTP that it does not appear in the requirment.

[andreaskatis]

Hello,

Could you share with us the variable mapping settings for the component that contains these requirements?

Thank you,

Andreas

[baobao1225]

Thank you very much

[baobao1225]

Thank you very much

[andreaskatis]

It is a bit too late here for me to play around with this example. In the meantime, since I see that "Compressor" is an input, I would suggest that you try and use it in the "condition" part of the FRETish statement, rather than "scope".

As for FTP, it stands for "first time point". It is essentially an internal flag whose truth designates whether we are in an initial system state, or not.

[baobao1225]

Thank you a lot,I change the requirments.And then they are sucessful.

condition,Compressor are input,and fan ,fan_toggled are output