Impossible de sélectionner les événements à préserver par la minimisation du graphe d'accessibilité (TTool du 22 janvier 2019)
Java(TM) SE Runtime Environment (build 1.8.0_05-b13) Java HotSpot(TM) 64-Bit Server VM (build 25.5-b02, mixed mode)
*** TTool version: 1.0beta -- build: 12919 date: 2019/01/22 03:02:14 CET ***
Experimental features activated
Configuration:
Launcher: LauncherPort: RTL: RTLHost: localhost RTLPath: /packages/RT-LOTOS.0.12/bin/rtl DTA2DOTPath: /packages/RT-LOTOS.0.12/bin/dta2dot RG2TLSAPath: /packages/RT-LOTOS.0.12/bin/rg2tlsa RGSTRAPPath: /packages/RT-LOTOS.0.12/bin/rgstrap
CADP: AldebaranHost: localhost AldebaranPath: /packages/cadp/com/aldebaran BcgioPath: /packages/cadp/bin.iX86/bcg_io BcgminPath: /packages/cadp/bin.iX86/bcg_min BisimulatorPath: /packages/cadp/com/bcg_open BcgmergePath: /packages/cadp/com/bcg_merge CaesarPath: /packages/cadp/bin.iX86/caesar CaesarOpenPath: /packages/cadp/com/caesar.open
Dotty: DOTTYHost: localhost DOTTYPath: /opt/csw/bin/dotty
UPPAAL: UPPAALCodeDirectory: ../uppaal/ UPPAALVerifierPATH: /packages/uppaal-4.0.11/verifyta UPPAALVerifierHOST: localhost UPPAALPropertyVerifMessage: UPPAALPropertyNotVerifMessage:
AVATAR (executable code): AVATARExecutableCodeDirectory: ../executablecode/ AVATARMPSoCCodeDirectory: ../MPSoC/ AVATARMPSoCCompileCommand: make -C ../MPSoC/ updateruntime updategeneratedcode compilesoclib AVATARExecutableCodeHost: localhost AVATARExecutableCodeCompileCommand: make AVATARExecutableCodeExecuteCommand: run.x AVATARExecutableSocLibCodeCompileCommand: make -C ../MPSoC/ updategeneratedcode compilesoclib AVATARExecutableSocLibCodeExecuteCommand: make -C ../MPSoC/ runsoclib AVATARExecutableSocLibCodeTraceCommand: make -C ../MPSoC/ runsoclib-trace AVATARExecutableSocLibCodeTraceFile: ../MPSoC/soclib/soclib/platform/topcells/caba-vgmn-mutekh_kernel_tutorial/trace
ProVerif: ProVerifCodeDirectory: ../proverif/ ProVerifVerifierPATH: ../../proverif ProVerifVerifierHOST: localhost
Your files (modeling, librairies, etc.): FILEPath: ../modeling DownloadedFILEPath: ../modeling LOTOSPath: ../lotos LIBPath: ../lib IMGPath: ../figures DocGenPath: ../document_generation GGraphPath: ../graphs TGraphPath: ../graphs
TTool update: TToolUpdateURL: TToolUpdateProxy: false TToolUpdateProxyPort: 8080 TToolUpdateProxyHost: To Be Completed
Java prototyping: JavaCodeDirectory: ../javacode JavaHeader: import java.sql.*; JavaCompilerPath: /usr/bin/javac TToolClassPath: ../javacode JavaExecutePath: /usr/bin/java SimuJavaCodeDirectory: TToolSimuClassPath:
DIPLODOCUS: SystemCCodeDirectory: ../simulators/c++2/ SystemCHost: localhost SystemCCodeCompileCommand: make -C ../simulators/c++2/ SystemCCodeExecuteCommand: ../simulators/c++2/run.x -ovcd ../simulators/c++2/vcddump.vcd SystemCCodeInteractiveExecuteCommand: ../simulators/c++2/run.x -server GTKWavePath: /opt/local/bin/gtkwave TMLCodeDirectory: ../tmlcode/ CCodeDirectory: ../CCode/ VCDPath: ../simulators/c++2/
Network calculus: NCDirectory: ../nc/
Plugins: Plugin path:
URLs: URL for loading models from network: http://ttool.telecom-paristech.fr/networkmodels/models.txt
Custom external commands: ExternalCommand1Host: localhost ExternalCommand1: gtkwave ../simulators/c++2/vcddump.vcd ExternalCommand2Host: localhost ExternalCommand2: /packages/uppaal4.0.11/uppaal ../uppaal/spec.xml
Information saved by TTool: LastOpenFile #0: ../modeling/AVATAR/CoffeeMachine_Avatar.xml LastOpenFile #1 (closed): LastOpenFile #2 (closed): LastOpenFile #3 (closed): LastOpenFile #4 (closed): LastOpenFile #5 (closed): LastOpenFile #6 (closed): LastOpenFile #7 (closed): LastOpenFile #8: LastOpenFile #9 (closed): LastWindowAttributesX: LastWindowAttributesY: LastWindowAttributesWidth: LastWindowAttributesHeight: LastWindowAttributesMax:
RG stylesheet configuration: ExternalServer
Debugging trace:
Preparing plugins
Server side of the launcher
Version: 0.61
Using port: 8375
Process running:0
Waiting for command
openLast=true
Autosaving in /Users/p.de-saqui-sannes/TTool/bin/../modeling/AVATAR/CoffeeMachine_Avatar.xml~
Loading model
Deactivating syntax checking
Autosaving in /Users/p.de-saqui-sannes/Downloads/2dronesTDMA_V_Final.xml~
Loading model
Deactivating syntax checking
Execute avatar model checker
Generating Avatar from TML
Thread started
String model checking
Reworking Avatar specification
***************************** Size of FIFO:1
*********************************** Size of FIFO=1
***************************** Size of FIFO:1
*********************************** Size of FIFO=1
Starting the model checking
Threads terminated
Model checking done
Model checking done
Expanding Path because of graphs
Autosaving in /Users/p.de-saqui-sannes/Downloads/2dronesTDMA_V_01_23_19.xml~
Exception in thread "Thread-16" java.lang.NoClassDefFoundError: rationals/NoSuchStateException
at ui.window.JFrameMinimize.computeListOfActions(JFrameMinimize.java:525)
at ui.window.JFrameMinimize.run(JFrameMinimize.java:553)
at java.lang.Thread.run(Thread.java:745)
Caused by: java.lang.ClassNotFoundException: rationals.NoSuchStateException
at java.net.URLClassLoader$1.run(URLClassLoader.java:372)
at java.net.URLClassLoader$1.run(URLClassLoader.java:361)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:360)
at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
Submitted by external user pdss@isae-supaero.fr