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/392Z3 DSE crashes on SmartCardProtocol2023-11-07T23:16:21ZMarvin HäuserZ3 DSE crashes on SmartCardProtocol# Summary
Performing Z3 DSE on the SmartCardProtocol project from the in-built repository crashes.
# Steps to reproduce
1. Load the SmartCardProtocol from the in-built repository.
2. Switch to Mapping1 and start Z3 DSE.
# What is th...# Summary
Performing Z3 DSE on the SmartCardProtocol project from the in-built repository crashes.
# Steps to reproduce
1. Load the SmartCardProtocol from the in-built repository.
2. Switch to Mapping1 and start Z3 DSE.
# What is the current bug behavior?
The process fails with the following error:
```
ERROR: Z3 Unknown Exception: Cannot invoke "tmltranslator.TMLTask.getOperation()" because "tmlTask" is null
```
# What is the expected correct behavior?
The process completes successfully, e.g.:
```
Optimized mapping found
The optimal mapping solution is:
(1) Spatial mapping of tasks:
TASK --> PLATFORM NODE
AppC__InterfaceDevice --> cpu0
AppC__SmartCard --> cpu0
AppC__TCPIP --> cpu0
AppC__Application --> cpu0
AppC__Timer --> cpu0
(2) Temporal mapping of tasks:
cpu0 : AppC__Timer at 0 ; AppC__Application at 1 ;
(3) Spatial mapping of channels onto controllers:
Channel(InterfaceDevice,SmartCard) --> cpu0
Channel(SmartCard,TCPIP) --> cpu0
Channel(SmartCard,InterfaceDevice) --> cpu0
Channel(TCPIP,TCPIP) --> cpu0
Channel(TCPIP,Application) --> cpu0
Channel(TCPIP,SmartCard) --> cpu0
Channel(Application,TCPIP) --> cpu0
```
# Possible fixes
The issue is masked or possibly resolved by rolling back the following change:
https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/merge_requests/107/diffs#75d2c997b1d082b003e6aa869cae021c48149d03_108_105
The change is undocumented and the intention is not obvious.
# Relevant logs and/or screenshots
Debugging the code check above with a "task name | writers.Empty() | readers.Empty()" scheme yields:
```
[tmltranslator.dsez3engine.InputInstance] AppC__Timer true true
[tmltranslator.dsez3engine.InputInstance] AppC__InterfaceDevice false false
[tmltranslator.dsez3engine.InputInstance] AppC__TCPIP false false
[tmltranslator.dsez3engine.InputInstance] fAppC__Application false true
[tmltranslator.dsez3engine.InputInstance] AppC__SmartCard false false
```
Thus, ``AppC__Timer`` is not picked as final task with the change from the MR, but is picked prior.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/391JDK 17: Migrate from Nashorn JS engine2023-11-10T18:24:49ZMarvin HäuserJDK 17: Migrate from Nashorn JS engineJDK 17 removed the Nashorn JavaScript engine [1]. This breaks DSE, which expects a JavaScript engine to be registered out-of-the-box. The most commonly accepted alternative to the removed Nashorn engine appears to be Graal.JS, with a mig...JDK 17 removed the Nashorn JavaScript engine [1]. This breaks DSE, which expects a JavaScript engine to be registered out-of-the-box. The most commonly accepted alternative to the removed Nashorn engine appears to be Graal.JS, with a migration guide readily available [2]. As ScriptEngine is not extensively used, the code changes required a fairly minimal to ship and consume Graal.JS along TTool. However, there are complicated considerations regarding combining it with GraalVM to improve performance:
* Optimal configuration requires experimental features to be enabled and module path upgrades [3].
* In a quick and dirty integration test, their class path isolation feature malfunctioned for unknown reasons.
[1] https://openjdk.org/jeps/372
[2] https://www.graalvm.org/latest/reference-manual/js/NashornMigrationGuide/
[3] https://www.graalvm.org/22.1/reference-manual/js/RunOnJDK/#graalvm-javascript-on-jdk-11https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/373Reset number of samples in a channel with wic command2022-09-09T11:56:08ZJawher JerrayReset number of samples in a channel with wic commandWe can reset the number of samples in a channel using the wic command by putting 0 as # of samples.
We probably could mention this feature in the wic command help.We can reset the number of samples in a channel using the wic command by putting 0 as # of samples.
We probably could mention this feature in the wic command help.https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/370Adding help for ports of diplodocus component2022-08-04T12:34:41ZLudovic ApvrilleAdding help for ports of diplodocus componentWe have to explain in particular the capacity and width of channelWe have to explain in particular the capacity and width of channelhttps://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/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/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/226Adding pragma for application period2020-02-28T19:48:51ZEmna GharbiAdding pragma for application periodAdding a pragma to indicate the period of an application.Adding a pragma to indicate the period of an application.Ludovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/206NoC: allow to enter the size of one flit2019-07-05T09:09:06ZLudovic ApvrilleNoC: allow to enter the size of one flitSize of one flit impacts:
* bus data size, CPU data size
* channel definition: width
Currently, 4 is the default valueSize of one flit impacts:
* bus data size, CPU data size
* channel definition: width
Currently, 4 is the default valueLudovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/205Ensure that a key is not mapped more than one time in a mem with the same ide...2021-01-14T10:23:08ZLudovic ApvrilleEnsure that a key is not mapped more than one time in a mem with the same identifierOtherwise, proverif fails to execute the generated spec.Otherwise, proverif fails to execute the generated spec.Ludovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/184Missing information on EXECI / EXECC transactions in SD generated from Diplod...2019-02-26T10:56:16ZLudovic ApvrilleMissing information on EXECI / EXECC transactions in SD generated from Diplodocus simulationsSee e.g. the simulation of the enclosed model
[TwoTaskModel.xml](/uploads/58af49ad5b65733431f324dab5d3b80d/TwoTaskModel.xml)See e.g. the simulation of the enclosed model
[TwoTaskModel.xml](/uploads/58af49ad5b65733431f324dab5d3b80d/TwoTaskModel.xml)Maysam ZoorMaysam Zoorhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/183Help for HW node parameters in DIPLODOCUS2021-01-20T12:09:41ZLudovic ApvrilleHelp for HW node parameters in DIPLODOCUSMinh Hiep Phamminh.pham@telecom-paristech.frMinh Hiep Phamminh.pham@telecom-paristech.frhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/166Bug in Diplodocus simulator when displaying simulation traces2018-11-14T15:25:51ZLudovic ApvrilleBug in Diplodocus simulator when displaying simulation tracesHow to reproduce (use attached model : [BugTraceDisplaying.xml](/uploads/8fd13adc790281cfad59c59a281aae90/BugTraceDisplaying.xml) )
- open the enclosed model
- select the architecture / mapping tab
- generate the simulation code (Beware:...How to reproduce (use attached model : [BugTraceDisplaying.xml](/uploads/8fd13adc790281cfad59c59a281aae90/BugTraceDisplaying.xml) )
- open the enclosed model
- select the architecture / mapping tab
- generate the simulation code (Beware: unselect the "Activate penalties")
- compile, execute the simulation to the end
- display the simulation trace "show simulation trace" at the top right of the window
The displayed trace is false because C0 should send 10 times the event but only one event is displayed. Other traces (e.g. HTML) are correct, so the problem is I guess in the displaying function.Maysam ZoorMaysam Zoorhttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/147Confidentiality generation for an origin fork channel fails2021-02-08T02:31:07ZLudovic ApvrilleConfidentiality generation for an origin fork channel failsIt usually results in
Exception in thread "Thread-23" java.lang.NullPointerException
at ui.SecurityGeneration.run(SecurityGeneration.java:260)
at java.lang.Thread.run(Thread.java:748)It usually results in
Exception in thread "Thread-23" java.lang.NullPointerException
at ui.SecurityGeneration.run(SecurityGeneration.java:260)
at java.lang.Thread.run(Thread.java:748)Letitia LiLetitia Lihttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/129Adding a deadline to requests2018-05-17T08:51:18ZLudovic ApvrilleAdding a deadline to requestsBeing able to specify a deadline to requests in functional diplodocus diagramsBeing able to specify a deadline to requests in functional diplodocus diagramsLudovic ApvrilleLudovic Apvrillehttps://gitlab.telecom-paris.fr/mbe-tools/TTool/-/issues/128Improvements on DIPLODOCUS Communication Patterns2018-05-16T13:38:00ZLudovic ApvrilleImprovements on DIPLODOCUS Communication Patterns- SD panels of CP: better differentiate between the different instances: the icon, and the graphical representation.
- Syntax checking activates wrong icons. BTW, what does the syntax checking perform?? Could we generate an internal avat...- SD panels of CP: better differentiate between the different instances: the icon, and the graphical representation.
- Syntax checking activates wrong icons. BTW, what does the syntax checking perform?? Could we generate an internal avatar representation and then simulate the CP?
- Specialize the instances (Storage, Control, Transfer) and the messages (TransferRequest, Read, Write, TransferTerminated). Read(size, ...), Write(size, ...), TR(size, ...), TT(...)
- Make a syntax checker: should verify the declaration of attributes, the validity of messages, the fact that there is a unique initiator which must be a Control instance
- Mapping of ports on CP: the user must precise to which storage of the CP the port corresponds. Thus, we can map different port. Finally, every time there is a write in a storage, we must know if this corresponds to a mapped port - in that case, the write must occur in a channel that is connected to the corresponding port.
- Automatically transform mapped CPS to a corresponding internal tml structure
- Automatically evaluate with a default mapping the syntax of a communication patternLudovic ApvrilleLudovic Apvrillehttps://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/69Allow to be able to disable action nodes in an activity diagram2018-08-23T08:31:29ZDominique BlouinAllow to be able to disable action nodes in an activity diagramLudovic ApvrilleLudovic Apvrille