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
Description of complex requirements #27
Comments
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>.
|
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? |
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>.
|
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>.
|
Thank you a lot,I understand your meaning,I am happy to talk with you. |
Hello, Could you share with us the variable mapping settings for the component that contains these requirements? Thank you, Andreas |
1 similar comment
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. |
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.
The text was updated successfully, but these errors were encountered: