TTool issueshttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues2022-03-24T12:27:44Zhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/359Model-checking from zigbee application suprisingly long2022-03-24T12:27:44ZLudovic ApvrilleModel-checking from zigbee application suprisingly longhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/358Update Diplodocus tutorial with internal model checker2022-03-24T09:48:26ZLudovic ApvrilleUpdate Diplodocus tutorial with internal model checkerhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/351window bash corrupted or fails2021-11-29T14:01:57ZEliott.Beaufilswindow bash corrupted or fails# Summary
(Summarize the bug encountered concisely)
# Steps to reproduce
(How one can reproduce the issue - this is very important)
# Example Project
(If possible, please create an example project here on GitLab.com that exhibits t...# Summary
(Summarize the bug encountered concisely)
# Steps to reproduce
(How one can reproduce the issue - this is very important)
# Example Project
(If possible, please create an example project here on GitLab.com that exhibits the problematic behaviour, and link to it here in the bug report)
(If you are using an older version of GitLab, this will also determine whether the bug has been fixed in a more recent version)
# What is the current bug behavior?
(What actually happens)
open window command prompt, and immediately closes
# What is the expected correct behavior?
(What you should see instead)
open window command prompt correctly or tool app (if there is one)
# Relevant logs and/or screenshots
cant take screenshots as it immediately closes
# Possible fixes
(If you can, link to the line of code that might be responsible for the problem)https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/347More than three next in choices (diplodocus AD, analysis AD)2021-11-19T10:35:17ZLudovic ApvrilleMore than three next in choices (diplodocus AD, analysis AD)Choices are limited to three choices. Having more would be better.Choices are limited to three choices. Having more would be better.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/345Images of help are not correctly displayed in ubuntu 20 LTS2021-11-03T09:22:36ZLudovic ApvrilleImages of help are not correctly displayed in ubuntu 20 LTShttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/344Graph visualization and manipulation is very slow in ubuntu 20 LTS2021-11-03T09:22:06ZLudovic ApvrilleGraph visualization and manipulation is very slow in ubuntu 20 LTShttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/343Improvement on formatting error for AVATAR methods and signals2022-03-09T10:32:13ZLudovic ApvrilleImprovement on formatting error for AVATAR methods and signalsFor instance, entering getSignal(int state) returns an error because "state" is a reserved keyword. The error should be more clear about that.For instance, entering getSignal(int state) returns an error because "state" is a reserved keyword. The error should be more clear about that.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/339Request to add a functionality in TTool2021-09-10T07:44:30ZDominique BlouinRequest to add a functionality in TToolHello,
I would like to have the possibility to create a state machine diagram directly. That is to say without the need to create a Block Definition Diagram before.
It could be useful in the case that we need to create a state machine ...Hello,
I would like to have the possibility to create a state machine diagram directly. That is to say without the need to create a Block Definition Diagram before.
It could be useful in the case that we need to create a state machine diagram in the Analysis phase and not in the Design phase.
Thank you in advance for your help.
Have a nice day,
Ombeline <br/> Submitted by external user ombeline.aiello@isae-supaero.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/335Linux menu shortcut2021-08-25T11:12:13ZMassimo.GismondiLinux menu shortcutHi!
Each time I start TTool on Linux I have to navigate to the folder, open a terminal and run it from the command line.
I added a menu shortcut to my menu, by putting a .desktop file in `~/.local/share/applications`
I post here my m...Hi!
Each time I start TTool on Linux I have to navigate to the folder, open a terminal and run it from the command line.
I added a menu shortcut to my menu, by putting a .desktop file in `~/.local/share/applications`
I post here my menu desktop file. Maybe it can be useful to someone.
```
[Desktop Entry]
Version=1.1
Type=Application
Name=TTool
Comment=A toolkit dedicated to the edition of UML, SysML diagrams and formal verification
Icon=/home/massimo/TTool/ttool_icon.png
Exec=/home/massimo/TTool/ttool_linux.exe
Path=/home/massimo/TTool
Actions=
Categories=Development;Utility;
Keywords=ttool;modelling;modeling;sysml;uml;
```
Can it be generated and copied to `~/.local/share/applications` in an install script and removed during uninstall maybe? I don't know where to get the current version number and icon path to fill in everything automatically.
Also, I renamed `ttool_linux.exe` to `ttool_linux.bin` or `ttool_linux.sh` on my system because Ubuntu was trying to start Wine when clicking on ithttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/328SysML V22021-07-16T15:26:04ZDominique BlouinSysML V2Bonjour,
Serait-il possible d'ajouter la notation textuelle de SysML V2 dans TTool ?
Merci d'avance.
Cordialement,
Ombeline AÏELLO (doctorante ISAE-SUPAERO)<br/> Submitted by external user ombeline.aiello@isae-supaero.frBonjour,
Serait-il possible d'ajouter la notation textuelle de SysML V2 dans TTool ?
Merci d'avance.
Cordialement,
Ombeline AÏELLO (doctorante ISAE-SUPAERO)<br/> Submitted by external user ombeline.aiello@isae-supaero.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/326Option "-explo" does not work as expected2021-06-18T14:54:58ZLe Van TruongOption "-explo" does not work as expected- In the enclosed model, when user click on run exploration button on the simulator, the output graph contains almost nothing, but in fact there should be more states and transitions.
[TemperatureSensor.xml](/uploads/47c2bc4adc3d92bd0aa1...- In the enclosed model, when user click on run exploration button on the simulator, the output graph contains almost nothing, but in fact there should be more states and transitions.
[TemperatureSensor.xml](/uploads/47c2bc4adc3d92bd0aa1ac4b93c513af/TemperatureSensor.xml)
- And in the below model, the -explo tend to infinity with many architecture tabs like "Architecture_enc_or" or "Architecture_hsm"
[ITSDemo.xml](/uploads/4fb1844b15d20cb779cb0797f4ed1044/ITSDemo.xml)Le Van TruongLe Van Truonghttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/320-nocolor --> menu2021-05-05T04:30:24ZDominique Blouin-nocolor --> menuHello,
I've been using TTool with the -nocolor option.
I would be grateful if you would make "nocolor" an option in a menu.
Thanks in anticipation.
Pierre de Saqui-Sannes
ISAE-SUPAERO, Toulouse, France<br/> Submitted by external user...Hello,
I've been using TTool with the -nocolor option.
I would be grateful if you would make "nocolor" an option in a menu.
Thanks in anticipation.
Pierre de Saqui-Sannes
ISAE-SUPAERO, Toulouse, France<br/> Submitted by external user pdss@isae-supaero.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/319Unexpected results when checking authenticity properties with ProVerif 2.022021-05-07T16:30:54ZBastien SultanUnexpected results when checking authenticity properties with ProVerif 2.02In Diplodocus modeling, authenticity properties seem to be unsatisfied when checking them on channels relying on private buses (security verification is done with the latest ProVerif version, i.e. 2.02pl1).
[bugAuthenticity.xml](/upload...In Diplodocus modeling, authenticity properties seem to be unsatisfied when checking them on channels relying on private buses (security verification is done with the latest ProVerif version, i.e. 2.02pl1).
[bugAuthenticity.xml](/uploads/dc9eb2b6cc360a48161f70ee90514ddf/bugAuthenticity.xml)https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/318Round Robin with Priority do not run as expected in some cases2021-05-03T12:16:54ZLe Van TruongRound Robin with Priority do not run as expected in some casesif a CPU uses RRPB scheduling, then transactions with virtual length = 0 belong to a task with high priority still being processed later than transactions with virtual length > 0 of lower priority tasks.
Expected result: transactions be...if a CPU uses RRPB scheduling, then transactions with virtual length = 0 belong to a task with high priority still being processed later than transactions with virtual length > 0 of lower priority tasks.
Expected result: transactions belong to higher priority task can be executed first.
Todo: Create a new RRPB called RoundRobin PriorityBase Not Preempted TaskLe Van TruongLe Van Truonghttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/313Upgrade Timeline diagram trace2021-08-09T09:49:56ZLe Van TruongUpgrade Timeline diagram traceThere are some ideas to upgrade the current timeline diagram:
* Add option to enable/disable the scale on idle time. => DONE
* Add option to display the trace in a selected duration/ => DONE
* Add a transparent layout that can show the p...There are some ideas to upgrade the current timeline diagram:
* Add option to enable/disable the scale on idle time. => DONE
* Add option to display the trace in a selected duration/ => DONE
* Add a transparent layout that can show the processors label and the label of all tasks.
* When moving the mouse pointer, the time is displayed next to the pointer only when it is located outside an activity => Display time stamp both inside or outside element block.
* When switching from a task to another one, the CPU is not idle, => change color e.g. task switching into gray for all OS.
- The zoom applies to the whole diagram, but just like in GTKWave => Make Zoom online on the X-axisLe Van TruongLe Van Truonghttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/305Saving the simulation context --> Restarting the simulation from where I stop...2021-07-01T11:33:06ZDominique BlouinSaving the simulation context --> Restarting the simulation from where I stopped beforeHello,
Below are actions I cannot perform with TTool/AVATAR:
1 - Starting a simulation
2 - Firing 1,000 transitions
3 - Saving the simulation context
4 - Exiting from TTool
5 - Restarting TTool
6 - Starting a simulation, not from the mo...Hello,
Below are actions I cannot perform with TTool/AVATAR:
1 - Starting a simulation
2 - Firing 1,000 transitions
3 - Saving the simulation context
4 - Exiting from TTool
5 - Restarting TTool
6 - Starting a simulation, not from the model's intial state, but from the context saved at step 3
Regards
Pierre de Saqui-Sannes
ISAE-SUPAERO, Toulouse, France<br/> Submitted by external user pdss@isae-supaero.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/294"__" Should be a reserved pragma in identifier2021-02-25T14:49:56ZLudovic Apvrille"__" Should be a reserved pragma in identifierAdding a warning or even an error, in the GUI or CLI would be betterAdding a warning or even an error, in the GUI or CLI would be betterhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/278Icon in Ubuntu 18.042021-01-24T21:10:10ZMatteo Bertolinomatteo.bertolino@telecom-paristech.frIcon in Ubuntu 18.04![Screenshot_from_2020-10-19_16-05-32](/uploads/b77cb5b67ac8065f6ecfe704c97fa209/Screenshot_from_2020-10-19_16-05-32.png)
There's a strange icon in Ubuntu 18.04 LTS, as shown in the attached picture.![Screenshot_from_2020-10-19_16-05-32](/uploads/b77cb5b67ac8065f6ecfe704c97fa209/Screenshot_from_2020-10-19_16-05-32.png)
There's a strange icon in Ubuntu 18.04 LTS, as shown in the attached picture.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/277Formal verification directly on AUT graphs2020-07-29T12:26:01ZAlessandro Tempia CalvinoFormal verification directly on AUT graphsReachability graphs can be generated in AUT format. It would be interesting to verify properties directly on AUT graphs.
In that case, we could work on string labels like:
* label1 --> label2
* A[] label1 or label2
where the labels ar...Reachability graphs can be generated in AUT format. It would be interesting to verify properties directly on AUT graphs.
In that case, we could work on string labels like:
* label1 --> label2
* A[] label1 or label2
where the labels are defined in the AUT file.
Practically, the verification mechanism is easier since it consists of one or multiple graph visits that check the reachability of labels and loops.
The usage of *SafetyProperty*, the evaluation mechanism of a property, and the fetching part of the algorithm in *AvatarModelChecker* could be partially reused.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/276Add a subtree dedicated to verification traces (AUT)2020-07-29T12:05:27ZAlessandro Tempia CalvinoAdd a subtree dedicated to verification traces (AUT)With realistic models, we tend to have many traces for each safety verification. It would be better to reduce/remove/move the space occupied by those traces in the reachability left tree?
Two ideas:
* have an icon just next to pragmas, t...With realistic models, we tend to have many traces for each safety verification. It would be better to reduce/remove/move the space occupied by those traces in the reachability left tree?
Two ideas:
* have an icon just next to pragmas, that would allow to open or to analyze the trace. Maybe simply a "t" at the right? But we should find a way to do it also for deadlocks and internal action loops.
* have one subtree of dedicated to verification traces, where elements can be easily managed
Also, both of them could be implemented.