Comments (16)
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:
Andreas
from fret.
from fret.
from fret.
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.
from fret.
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
from fret.
from fret.
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
from fret.
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.
from fret.
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.
from fret.
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.
from fret.
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
from fret.
hi@andreaskatis
signal is an input variable and A is a output variable
from fret.
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
from fret.
Hello @baobao1225,
Just wanted to check-in with you. Did the latest version of our master
branch help fix your issue?
Best Regards,
Andreas
from fret.
Hello@andreaskatis
I don't know how to upgrade Fret.Do you have any advice?
Thank you very much
from fret.
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
from fret.
Related Issues (20)
- Unsuccessful Installation HOT 3
- Error "incompatible architecture (have (x86_64), need (arm64e))" trying to start FRET on an M1 machine HOT 3
- Export requirements status field in json format HOT 4
- Electron GPU initialization fails on Ubuntu 22.04 HOT 6
- could not install fret HOT 5
- Realizability GUI issue HOT 5
- Broken link in docs HOT 2
- Error on Install: regex.h no such file or directory HOT 3
- Installation on Mac M1 Monterey throwing webpack/native dependency errors HOT 8
- Bug: All Caps "Immediately" keyword causes blank screen HOT 4
- Unable to run executable built with Docker on Ubuntu 22.04 HOT 2
- Requirement Description Text Box Stops Various Keys (and highlighting) from Working HOT 4
- Trailing bit of requirement after a colon HOT 2
- Search Bar Doesn't Respond to Enter Key HOT 3
- I get this error when I run npm start HOT 9
- Templates Lack Syntax Highlighting and Structure Uneditable HOT 2
- pmLTL and fmLTL don't seem to be equivalent HOT 3
- Docker build issue for v2.9.0 - import error HOT 4
- Installation fails HOT 4
- Unexpected behavior in the realizability check HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from fret.