Update on TTool -> Bug on model checker

executablecode/Makefile.forsoclib

@@ -5,13 +5,13 @@ PATH+=/opt/mutekh/bin
 export PATH
 
 updateruntime:
-	cp ~/TURTLE/executablecode/src/*.c ~/Prog/mutekh/libavatar/
-	cp ~/TURTLE/executablecode/src/*.h ~/Prog/mutekh/libavatar/include/  
+	cp ~/TTool/executablecode/src/*.c ~/Prog/mutekh/libavatar/
+	cp ~/TTool/executablecode/src/*.h ~/Prog/mutekh/libavatar/include/  
 
 updategeneratedcode:
-	cp ~/TURTLE/executablecode/generated_src/*.h ~/Prog/mutekh/examples/avatar
-	cp ~/TURTLE/executablecode/generated_src/*.c ~/Prog/mutekh/examples/avatar	
-	cp ~/TURTLE/executablecode/Makefile.soclib ~/Prog/mutekh/examples/avatar/Makefile
+	cp ~/TTool/executablecode/generated_src/*.h ~/Prog/mutekh/examples/avatar
+	cp ~/TTool/executablecode/generated_src/*.c ~/Prog/mutekh/examples/avatar	
+	cp ~/TTool/executablecode/Makefile.soclib ~/Prog/mutekh/examples/avatar/Makefile
 
 compilesoclib:
 	cd ~/Prog/mutekh; make CONF=examples/avatar/config BUILD=soclib-$(MUTEKH_CPU):pf-tutorial

executablecode/Makefile.src

-SRCS = generated_src/main.c generated_src/TestBench.c generated_src/EmergencySimulator.c generated_src/CarPositionSimulator.c generated_src/GPSSensor.c generated_src/RadarSensor.c generated_src/SpeedSensor.c generated_src/Communication.c generated_src/CorrectnessChecking.c generated_src/NeighbourhoodTableManagement.c generated_src/DSRSC_Management.c generated_src/PTC.c generated_src/DrivingPowerReductionStrategy.c generated_src/BCU.c generated_src/BrakeManagement.c generated_src/DangerAvoidanceStrategy.c generated_src/CSCU.c generated_src/VehiculeDynamicsManagement.c generated_src/PlausibilityCheck.c generated_src/ObjectListManagement.c 
\ No newline at end of file
+SRCS = generated_src/main.c generated_src/ObserverProp1.c generated_src/RemotelyControlledMicrowave.c generated_src/MicroWaveOven.c generated_src/Bell.c generated_src/ControlPanel.c generated_src/Controller.c generated_src/Magnetron.c generated_src/Door.c 
\ No newline at end of file

executablecode/src/tracemanager.h

 #ifndef TRACEMANAGER_H
-#define TRACEMANANER_H
+#define TRACEMANAGER_H
 
 #include "request.h"
 

preinstallTTool/TTool_Macosx/TTool/bin/config.xml

@@ -50,4 +50,6 @@
 <LastWindowAttributes x="240" y="107" width="1414" height="777" max="false" />
 
 
+<ProVerifHash data=""/>
+
 </TURTLECONFIGURATION>

src/avatartranslator/AvatarStateMachine.java

@@ -213,7 +213,7 @@ public class AvatarStateMachine extends AvatarElement {
 
                 // If the next and previous are non states
                 if ((previous != null) && (next != null)) {
-                    if ((!(previous instanceof AvatarState)) && (!(next instanceof AvatarState))) {
+                    if ((!(previous instanceof AvatarStateElement)) && (!(next instanceof AvatarStateElement))) {
                         // We create an intermediate state
                         AvatarState state = new AvatarState("IntermediateState__" + id, elt.getReferenceObject());
                         toAdd.add(state);

src/avatartranslator/modelchecker/AvatarModelChecker.java

@@ -816,8 +816,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
 
         if ((AvatarTransition.isActionType(type)) || (type == AvatarTransition.TYPE_EMPTY)) {
             _st.infoForGraph = executeActionTransition(_previousState, _newState, _st);
+	    return ;
         } else if (type == AvatarTransition.TYPE_SEND_SYNC) {
             _st.infoForGraph =  executeSyncTransition(_previousState, _newState, _st);
+	    return ;
         }
 
 	_st.infoForGraph = "not implemented";