How to understand the result of diagnose?

[Dustin-Grandret]

I know my fretish has a problem with the use of 'after n time unit '. It seems not to work if "after n time unit" holds for many times within interval n , for RTGIL semantics of "after n time unit" requires !RES holds within n time unit. However, I do not understand the diagnosis since output variable C is always false. And is there any way to require RES to be true only after 2s? (At other time points, values of RES are non-deterministic)

fretish I wrote:

data types and id types of variables:

result of "diagnose":

[andreaskatis]

Hello @Dustin-Grandret ,

Thank you for trying out FRET, and submitting this issue! This is a very interesting example, and we will have to take a closer look at it before we can give you a definitive answer. Our RTGIL semantics expert is unavailable until next Wednesday, so we may not be able to figure this one out until then.

Edit: I forgot to mention that it may be worth trying the simulator to make sure that the requirements evaluate as you'd like them to. Please keep in mind that you will need to rename A to something else to get sound results, because it is a reserved operator in NuSMV, and this fact is not properly handled in the translation process. You can read more about simulator restrictions here:

https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/UsingTheSimulator/ltlsim.md#restrictions

Andreas

[Dustin-Grandret]

Hi @andreaskatis,
Thank you for your tips on naming variables. FRET is one of your team's excellent works, looking forward to your response and the future development of FRET.

Dustin

[artimid]

Hi Dustin, Here is what I believe happens in your example: Variable A is an input so it is uncontrollable. In the diagnose result, variable A is true at step 0, which per the first requirement (R1), expects variable B to be true thereafter. The second requirement (R2) states that in all intervals defined by variable B being true ("while B" means "in mode" where mode is determined by B being true), unless A is true, C should occur after 2 time units, which, as you also point out, means that C should not occur within 2 time units. We have two continuous time points (step1) and (step2) where B is true and A is false, so requirement 2 is triggered at both points. As a consequence, when the trigger at step 1 will require C to become true, the trigger at step 2 will still require C to be false, which is a problem. To avoid violating R2, the counterexample makes B false at step 3, so we are no longer in the mode interval (while B), and we no longer need to satisfy the "after 2 time steps" requirement since the mode interval is too short. That, however, violates the first requirement (R1), which expects B to remain true. One could say - "why did it not make A true in order to not trigger requirement 2"? A is an input, so the requirements should be realizable irrespective of A's value. It is a bit convoluted, but I hope it helps. Dimitra

…

On Tue, Apr 12, 2022 at 6:05 AM Dustin-Grandret ***@***.***> wrote: I know my fretish has a problem with the use of '*after n time unit* '. It seems not to work if "*after n time unit*" holds for many times within interval n , *for RTGIL semantics of "after n time unit" requires !RES holds within n time unit*. However, I do not understand the diagnosis since output variable C is always false. And is there any way to require RES to be true only after 2s? (At other time points, values of RES are non-deterministic) fretish I wrote: [image: image] <https://user-images.githubusercontent.com/54626800/162938641-aff9c084-980f-40b0-8ea4-b38988f96bc2.png> data types and id types of variables: [image: image] <https://user-images.githubusercontent.com/54626800/162938919-9536f937-5bfd-4acf-9d7c-4f3640c066d0.png> result of "diagnose": [image: image] <https://user-images.githubusercontent.com/54626800/162939093-eaab8080-99f7-4eaf-aeb0-ce52452c8a57.png> — Reply to this email directly, view it on GitHub <#41>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACGVMKID46HFGTPJWCIKOILVEVKGVANCNFSM5TGZ746A> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[artimid]

@Dustin-Grandret <https://github.com/Dustin-Grandret> On Tue, Apr 12, 2022 at 7:26 PM Dimitra Giannakopoulou < ***@***.***> wrote:

…

Hi Dustin, Here is what I believe happens in your example: Variable A is an input so it is uncontrollable. In the diagnose result, variable A is true at step 0, which per the first requirement (R1), expects variable B to be true thereafter. The second requirement (R2) states that in all intervals defined by variable B being true ("while B" means "in mode" where mode is determined by B being true), unless A is true, C should occur after 2 time units, which, as you also point out, means that C should not occur within 2 time units. We have two continuous time points (step1) and (step2) where B is true and A is false, so requirement 2 is triggered at both points. As a consequence, when the trigger at step 1 will require C to become true, the trigger at step 2 will still require C to be false, which is a problem. To avoid violating R2, the counterexample makes B false at step 3, so we are no longer in the mode interval (while B), and we no longer need to satisfy the "after 2 time steps" requirement since the mode interval is too short. That, however, violates the first requirement (R1), which expects B to remain true. One could say - "why did it not make A true in order to not trigger requirement 2"? A is an input, so the requirements should be realizable irrespective of A's value. It is a bit convoluted, but I hope it helps. Dimitra On Tue, Apr 12, 2022 at 6:05 AM Dustin-Grandret ***@***.***> wrote: > I know my fretish has a problem with the use of '*after n time unit* '. > It seems not to work if "*after n time unit*" holds for many times > within interval n , *for RTGIL semantics of "after n time unit" requires > !RES holds within n time unit*. However, I do not understand the > diagnosis since output variable C is always false. And is there any way to > require RES to be true only after 2s? (At other time points, values of RES > are non-deterministic) > > fretish I wrote: > [image: image] > <https://user-images.githubusercontent.com/54626800/162938641-aff9c084-980f-40b0-8ea4-b38988f96bc2.png> > > data types and id types of variables: > [image: image] > <https://user-images.githubusercontent.com/54626800/162938919-9536f937-5bfd-4acf-9d7c-4f3640c066d0.png> > > result of "diagnose": > [image: image] > <https://user-images.githubusercontent.com/54626800/162939093-eaab8080-99f7-4eaf-aeb0-ce52452c8a57.png> > > — > Reply to this email directly, view it on GitHub > <#41>, or unsubscribe > <https://github.com/notifications/unsubscribe-auth/ACGVMKID46HFGTPJWCIKOILVEVKGVANCNFSM5TGZ746A> > . > You are receiving this because you are subscribed to this thread.Message > ID: ***@***.***> >

[artimid]

Hi again @Dustin-Grandret <https://github.com/Dustin-Grandret>, I do not have FRET with me right now to test things, and I do not recall exactly how unless works (it was introduced later) - but if you change unless to say if !A, what does diagnose return? It just occurred to me that FRET conditions are triggered on change from false to true, so in the example trace you have, I would expect the condition trigger to hold only at step 1. Of course, one could still reconstruct a different counterexample by changing the values of A to have the trigger occur at multiple points. Dimitra On Tue, Apr 12, 2022 at 7:29 PM Dimitra Giannakopoulou < ***@***.***> wrote:

…

@Dustin-Grandret <https://github.com/Dustin-Grandret> On Tue, Apr 12, 2022 at 7:26 PM Dimitra Giannakopoulou < ***@***.***> wrote: > Hi Dustin, > > Here is what I believe happens in your example: > > Variable A is an input so it is uncontrollable. > In the diagnose result, variable A is true at step 0, which per the first > requirement (R1), expects variable B to be true thereafter. > > The second requirement (R2) states that in all intervals defined by > variable B being true ("while B" means "in mode" where mode is determined > by B being true), unless A is true, C should occur after 2 time units, > which, as you also point out, means that C should not occur within 2 time > units. We have two continuous time points (step1) and (step2) where B is > true and A is false, so requirement 2 is triggered at both points. As a > consequence, when the trigger at step 1 will require C to become true, the > trigger at step 2 will still require C to be false, which is a problem. To > avoid violating R2, the counterexample makes B false at step 3, so we are > no longer in the mode interval (while B), and we no longer need to satisfy > the "after 2 time steps" requirement since the mode interval is too short. > > That, however, violates the first requirement (R1), which expects B to > remain true. One could say - "why did it not make A true in order to not > trigger requirement 2"? A is an input, so the requirements should be > realizable irrespective of A's value. > > It is a bit convoluted, but I hope it helps. > > Dimitra > > > On Tue, Apr 12, 2022 at 6:05 AM Dustin-Grandret ***@***.***> > wrote: > >> I know my fretish has a problem with the use of '*after n time unit* '. >> It seems not to work if "*after n time unit*" holds for many times >> within interval n , *for RTGIL semantics of "after n time unit" >> requires !RES holds within n time unit*. However, I do not understand >> the diagnosis since output variable C is always false. And is there any way >> to require RES to be true only after 2s? (At other time points, values of >> RES are non-deterministic) >> >> fretish I wrote: >> [image: image] >> <https://user-images.githubusercontent.com/54626800/162938641-aff9c084-980f-40b0-8ea4-b38988f96bc2.png> >> >> data types and id types of variables: >> [image: image] >> <https://user-images.githubusercontent.com/54626800/162938919-9536f937-5bfd-4acf-9d7c-4f3640c066d0.png> >> >> result of "diagnose": >> [image: image] >> <https://user-images.githubusercontent.com/54626800/162939093-eaab8080-99f7-4eaf-aeb0-ce52452c8a57.png> >> >> — >> Reply to this email directly, view it on GitHub >> <#41>, or unsubscribe >> <https://github.com/notifications/unsubscribe-auth/ACGVMKID46HFGTPJWCIKOILVEVKGVANCNFSM5TGZ746A> >> . >> You are receiving this because you are subscribed to this thread.Message >> ID: ***@***.***> >> >

[andreaskatis]

Hi @Dustin-Grandret ,

Dimitra was not sure whether you were notified, so I just wanted to make sure that you do with this post. Please look at Dimitra's responses and let us know if you have more questions.

I should add that the query that generates the counterexample trace is essentially checking whether we can find an execution trace of length N, which can only be extended with transitions to states where at least one requirement is violated. This query only comes after we have proved that the requirements are indeed unrealizable, i.e. there is no system that can actually keep satisfying the requirements given uncontrollable inputs from its environment.

The counterexample is a single witness depicting how things can "go wrong" , and there can be more, some being more intuitive, some less. Because of this we are actively trying to improve this aspect of diagnosis and, in fact, we will be very soon introducing the ability to use the simulator to interact specifically with conflicting requirements. Please stay tuned!

There's one more question of yours that we need to answer, regarding the possibility of requiring RES to only be true after 2 steps. We will get back to you as soon as possible on this.

[Dustin-Grandret]

Thank you again, Dimitra and Andreas.

I understand your explanation(#41 (comment)) on the counterexamples.

In order to solve this conflict, there may be two methods: one is to increase the constraint on A (I noticed that the assertion can be declared by adding assertion to the ID of the requirement according to the source code of turning fretish to .lus). The other is to relax the condition of after n time unit, which may be realized in a more complex form through multiple requirements. This is what I am trying to do at present, and It would be nice if there were a syntax sugar for it(require RES is true only at the time point n+1). These two solutions could correspond to different semantics.

If I have a mistake about the usage of "assumption", please point out.

---

unless COND and If !COND seem to have the same behavior

[andreaskatis]

Hi @Dustin-Grandret ,

Your understanding regarding the use of "assumption" is correct. Currently, requirements that have the word "assumption" in their ID are considered as assumptions for the purposes of realizability checking. Assumptions are expected to be constraints over the environment.

Your general understanding regarding how to repair unrealizability is also correct. You can either strengthen the environment assumptions (i.e. add constraints about A in your example), or weaken the system guarantees (i.e. constraints over B and C).

I am not sure what you mean by relaxing after n time unit, though. It would be good if you could provide a more concrete example on this. They way that I understand this is that you would like to say something along the lines "C doesn't have to be true exactly after 2 steps, it can be true later than that, and that is ok".

Please keep in mind that the counterexamples that you see are not the only kinds of traces leading to some violation. There can be many different traces that represent other kinds of behavior. To truly understand unrealizability, you may need the collection of all these different kinds of counterexamples. In your example, another violating trace is one where A is toggled to false more than once before C becomes true 2 seconds after the first toggle of A (see attached). This counterexample alone suggests that weakening the guarantees may not be enough to repair this specification.

[Dustin-Grandret]

Hi @andreaskatis,

I'm sorry that my statement may make you misunderstand what I mean by relaxing after n time units. I want to use relaxing the condition of after n time units to express that requirement requires RES to be true only after n+1 time unit, and at other time points, values of RES are non-deterministic.

--
e.g.
turns
requires RES to be false at the time point k, where k <= n, RES to be true at the time point n+1.(when AA the system shall after n time units satisfy BB.)

to:
requires RES to be true at the time point n+1.(may be realized in a more complex form through multiple requirements)

---

Please keep in mind that the counterexamples that you see are not the only kinds of traces leading to some violation. There can be many different traces that represent other kinds of behavior. To truly understand unrealizability, you may need the collection of all these different kinds of counterexamples.

Thanks, this is very helpful to fix bugs.

[baobao1225]

I know my fretish has a problem with the use of 'after n time unit ' . It seems not to work if "after n time unit" holds for many times within interval n , for RTGIL semantics of "after n time unit" requires !RES holds within n time unit. And, I add some assumptions in Fret.However, I do not understand the diagnosis since output variable A is always false.

[andreaskatis]

Hi @baobao1225 ,

We will look into this. For the time being, can you please confirm that variable signal is an input variable? The counterexample seems to indicate this, but it is not clear from the information you've provided.

Thanks,

Andreas

[baobao1225]

hi@andreaskatis
signal is an input variable and A is a output variable

[andreaskatis]

Hi @baobao1225

Are you using the latest 'master' from our repository? Running realizability on these requirements returned a realizable result for me, using JKind.

The latest 'master' has introduced some fixes to Lustre definitions of temporal operators, including ones that you exercise in the example requirements. Perhaps this is causing the discrepancy in the results that we see.

Best Regards,

Andreas

[andreaskatis]

Hello @baobao1225,

Just wanted to check-in with you. Did the latest version of our master branch help fix your issue?

Best Regards,

Andreas

[baobao1225]

Hello@andreaskatis
I don't know how to upgrade Fret.Do you have any advice?
Thank you very much

[andreaskatis]

Hi @baobao1225 ,

In the following I assume you installed from source, by cloning the git repository.

While inside the path of the cloned repository, run git pull. This should pull the most recent version from github. After this, you may or may not need to run npm run fret-reinstall , under fret/fret-electron.

If you encounter any problems, please let me know.

Best Regards,

Andreas