Comments (3)
Hi,
sorry for the lag, it looks like a bug as there is no reason we lose events in the ETF scenario, I'll investigate and reproduce today and notify here if/when it's patched.
Some tips : for more readable traces you usually want to activate "-backward" as forward time operators are more efficient for solving but make for harder traces to read.
You might also consider using/generating a GAL input for your models, that is the currently recommended approach, we can then regenerate a PINS model from a GAL if you want to interact with LTSmin.
I'll post here when I4ve debugged you example.
from itstools.
So, your ETF files are unusual they use features that are not well supported such as action labels and a one-hot encoding for your automaton + no locality/a single transition group.
So this ETF input has mostly been used with models that came thru LTSmin from Divine models, the procedure to build traces actually has quite a bit of code to assign unlabeled transitions to a "process" a concept that exists in Divine but not really in ETF.
While I would be willing to improve our support for this type of ETF file, it would have to be because it is truly useful for you, but perhaps we can find another path to handle your models e.g. GAL.
trace.zip
here is a GAL file for this model + readable trace. Formula 3 is trivially false because initial state does not respect the condition.
I just wrote the file by looking at your PNG, then right-click -> Run As -> ITS-model check
Then right click again -> run as -> run configurations
Switch to its-ctl on the "model selection" tab and add witness and backward on "CTL" tab and run.
from itstools.
Hi Yann,
Thank you for the investigation. At this moment i can't justify to spend a lot of effort in improving this. :-).
The models that i am working on are not coming from Divine, nor LTSMIN. I only have an explicit model and i needed a way to encoded it for a model checker. That is why i was using ETF.
I will investigate the usability of the skeleton you provided to see i if can encode my explicit model in GAL. I also like the log with the trace: this is good to comprehend, better than the log from the etf version of the toy model.
Thank you.
Carlo
from itstools.
Related Issues (15)
- Extend flags that can be passed to ITS model check HOT 2
- Archive versions of the update site / release HOT 3
- Sequential composition of assignments?? HOT 6
- urgent channels in XTA HOT 2
- Promela to GAL transformation error HOT 2
- System invariants in GAL HOT 10
- Derived state variables HOT 11
- Run as its -model-check only runs one of ltl, reachability or CTL HOT 1
- Chain transformations
- specify target properties separately from model
- limited quantifiers in properties HOT 3
- bug during simplification with nested arrayRefs HOT 1
- missing dynamic library when installing its-reach on a fresh linux HOT 5
- NPE whe trying to run its reach or flatten HOT 4
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 itstools.