TTool issueshttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues2023-12-07T15:20:50Zhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/393Proverif specification generation fails when using Timer type in messages2023-12-07T15:20:50ZLudovic ApvrilleProverif specification generation fails when using Timer type in messagesSo types in functions are not checked for before proverif generation (e.g., syntax checking)So types in functions are not checked for before proverif generation (e.g., syntax checking)https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/388Question: Does TTool support the Requirements Interchange Format?2023-09-21T06:29:54ZDominique BlouinQuestion: Does TTool support the Requirements Interchange Format?Hello
Does TTool support the Requirements Interchange Format (ReqIF), proposed by OMG (https://www.omg.org/reqif/)?
Best regards
Maisa
<br/> Submitted by external user maisa.cietto@usp.brHello
Does TTool support the Requirements Interchange Format (ReqIF), proposed by OMG (https://www.omg.org/reqif/)?
Best regards
Maisa
<br/> Submitted by external user maisa.cietto@usp.brhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/361Avatar-to-proverif generates an unvalid proverif specification because invali...2022-05-02T16:02:52ZLudovic ApvrilleAvatar-to-proverif generates an unvalid proverif specification because invalid guards for proverif are not detectedFor instance, (a==b) != false generates a faulty proverif specificationFor instance, (a==b) != false generates a faulty proverif specificationhttps://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/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/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/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.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/272Bactrackig of verification results --> scenario simulation2020-07-08T15:33:35ZDominique BlouinBactrackig of verification results --> scenario simulationHi,
How to trace back when a property (pragma) is not satisfied?
Today: the question is answered in the form of a graph.
Problem: how to relate the graph to the state machines of the SysML model?
My proposal: generate a simulation scena...Hi,
How to trace back when a property (pragma) is not satisfied?
Today: the question is answered in the form of a graph.
Problem: how to relate the graph to the state machines of the SysML model?
My proposal: generate a simulation scenario in order to simulate the states machines and show the way to a state where the property is not satisfied.
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/257Co-édition de diagrammes2020-07-06T10:20:10ZDominique BlouinCo-édition de diagrammesBonjour,
Est-il envisageable d'autoriser plusieurs personnes à éditer "en même temps" un ou plusieurs diagrammes d'un même modèle ?
Cordialement
Pierre de Saqui-Sannes, ISAE-SUPAERO, Toulouse, France<br/> Submitted by external user pd...Bonjour,
Est-il envisageable d'autoriser plusieurs personnes à éditer "en même temps" un ou plusieurs diagrammes d'un même modèle ?
Cordialement
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/165Data Structure in a Data Structure (suggestion, not a bug)2020-07-06T10:10:41ZDominique BlouinData Structure in a Data Structure (suggestion, not a bug)Hi!
My message addresses class diagrams and more precisely data stuctures.
I'd like to declare Point made up of 2 coordinates, and reuse Point as the type of four "fileds" (attributes) declared in data structure Rectangle.
In brief, a d...Hi!
My message addresses class diagrams and more precisely data stuctures.
I'd like to declare Point made up of 2 coordinates, and reuse Point as the type of four "fileds" (attributes) declared in data structure Rectangle.
In brief, a data structure whose fields are typed by a type defined by another data stucture.
Thanks in anticipation.
Pierre de Saqui-Sannes
<br/> Submitted by external user pdss@isae-supaero.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/84Show a reachability scenario when a state is reachable2021-01-19T17:26:03ZLudovic ApvrilleShow a reachability scenario when a state is reachableBe able to click on a reachability icon, and display a sequence diagram showing that reachability ..Be able to click on a reachability icon, and display a sequence diagram showing that reachability ..Ludovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/78Forbidden identifiers2019-10-18T13:24:22ZLudovic ApvrilleForbidden identifiers"state" should be a forbidden identifier for all diagrams (UPPAAL uses "state" as a reserved identifier). "state" should be a forbidden identifier for all diagrams (UPPAAL uses "state" as a reserved identifier). Moemoea FiérinMoemoea Fiérinhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/52Model refactoring2018-01-13T00:10:20ZLudovic ApvrilleModel refactoringHandling refactoring in models. For instance, when changing the name of a signal in an AVATAR block, all reference to this signal are updated.
Fabien: Named refactoring is now handled in DIPLODOCUS. Still needs to be done for AVATAR.Handling refactoring in models. For instance, when changing the name of a signal in an AVATAR block, all reference to this signal are updated.
Fabien: Named refactoring is now handled in DIPLODOCUS. Still needs to be done for AVATAR.Dominique BlouinDominique Blouinhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/51Handling loops and alternatives in Sequence Diagrams2018-04-16T15:17:27ZLudovic ApvrilleHandling loops and alternatives in Sequence DiagramsLudovic ApvrilleLudovic Apvrille