...
 
Commits (36)
12760
\ No newline at end of file
12775
\ No newline at end of file
SRCS = generated_src/main.c generated_src/AvatarSignal.c generated_src/AvatarRelation.c generated_src/AvatarElement.c generated_src/AvatarMethod.c generated_src/AvatarAction.c generated_src/AvatarGuard.c generated_src/AvatarTransition.c generated_src/AvatarState.c generated_src/AvatarStateMachine.c generated_src/AvatarPragma.c generated_src/AvatarConstant.c generated_src/AvatarAttribute.c generated_src/AvatarBlock.c generated_src/AvatarSpecification.c
\ No newline at end of file
SRCS = generated_src/main.c generated_src/AlarmActuator.c generated_src/PressureSensor.c generated_src/PressureController.c generated_src/AlarmManager.c generated_src/MainController.c generated_src/Timer__alarmTimer__AlarmManager.c
\ No newline at end of file
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
......@@ -52,11 +52,11 @@ public class AvatarConstant extends AvatarTerm {
public static final AvatarConstant FALSE = new AvatarConstant ("false", null);
public boolean isLeftHand (){
return false;
return false;
}
public AvatarConstant (String _name, Object _referenceObject) {
super (_name, _referenceObject);
super(_name, _referenceObject);
}
@Override
......
......@@ -177,7 +177,7 @@ public abstract class AvatarGuard {
}
}
for (String delim: new String[] {"==", "!="}) {
for (String delim: new String[] {"==", "!=", "<", ">"}) {
int indexBinaryOp = sane.indexOf (delim);
if (indexBinaryOp != -1) {
AvatarTerm firstTerm = AvatarTerm.createFromString (block, sane.substring (0, indexBinaryOp));
......
......@@ -79,12 +79,9 @@ public class AvatarSimpleGuardMono extends AvatarSimpleGuard {
// {
// }
if (this.term instanceof AvatarAttribute)
{
if (this.term instanceof AvatarAttribute) {
this.term = attributesMapping.get(this.term);
}
else
{
} else {
this.term.replaceAttributes (attributesMapping);
}
}
......
......@@ -607,7 +607,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute the hash of the new state, and create the link to the right next state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
action += " [" + tr.clockMin + " ..." + clockMax + "]";
action += " [" + tr.clockMin + "..." + clockMax + "]";
link.action = action;
newState.computeHash(blockValues);
//SpecificationState similar = states.get(newState.getHash(blockValues));
......
......@@ -349,7 +349,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return null;
if (_guard instanceof AvatarSimpleGuardMono) {
//TraceManager.addDev("SimpleGuardMono:" + _guard);
String term = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardMono) _guard).getTerm (), attributeCmp);
//TraceManager.addDev("guard/ term=" + term);
if (term != null)
return term + " = " + TRUE;
......@@ -357,13 +359,19 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarSimpleGuardDuo) {
//TraceManager.addDev("SimpleGuardDuo");
String delim = null;
String termA = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermA (), attributeCmp);
String termB = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermB (), attributeCmp);
if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("=="))
delim = "=";
/*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("<"))
delim = "<";*/
else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("!="))
delim = "<>";
/*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals (">"))
delim = ">";*/
if (termA != null && termB != null && delim != null)
return termA + " " + delim + " " + termB;
......@@ -372,6 +380,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarUnaryGuard) {
//TraceManager.addDev("UnaryGuard");
String unary = ((AvatarUnaryGuard) _guard).getUnaryOp ();
AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard ();
......@@ -392,6 +401,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarBinaryGuard) {
//TraceManager.addDev("BinaryGuard");
String delim = ((AvatarBinaryGuard) _guard).getBinaryOp ();
AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA ();
AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB ();
......@@ -411,6 +421,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarConstantGuard) {
//TraceManager.addDev("ConstantGuard");
AvatarConstantGuard constant = (AvatarConstantGuard) _guard;
if (constant.getConstant () == AvatarConstant.TRUE)
return "true";
......@@ -1169,6 +1180,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Check if the transition is guarded
if (_asme.isGuarded() && !arg.lastASME.hasElseChoiceType1 ()) {
TraceManager.addDev("Analyzing GUARD: " + _asme.getGuard() + " real guard=" + _asme.getGuard().getRealGuard (arg.lastASME));
String tmp = AVATAR2ProVerif.translateGuard(_asme.getGuard().getRealGuard (arg.lastASME), arg.attributeCmp);
if (tmp != null) {
TraceManager.addDev("| | transition is guarded by " + tmp);
......
......@@ -188,7 +188,7 @@ public class SpecConfigTTool {
AVATARExecutableSoclibCodeCompileCommand = ConfigurationTTool.AVATARExecutableSoclibCodeCompileCommand.replace(ConfigurationTTool.AVATARMPSoCCodeDirectory, AVATARMPSoCCompileCommand);
AVATARExecutableSoclibCodeExecuteCommand = ConfigurationTTool.AVATARExecutableSoclibCodeExecuteCommand.replace(ConfigurationTTool.AVATARMPSoCCodeDirectory, AVATARMPSoCCompileCommand);
AVATARExecutableSoclibCodeTraceCommand = ConfigurationTTool.AVATARExecutableSoclibCodeTraceCommand.replace(ConfigurationTTool.AVATARMPSoCCodeDirectory, AVATARMPSoCCompileCommand);
ExternalCommand1 = ConfigurationTTool.ExternalCommand1.replace(ConfigurationTTool.VCDPath, SpecConfigTTool.VCDPath);
//ExternalCommand1 = ConfigurationTTool.ExternalCommand1.replace(ConfigurationTTool.VCDPath, SpecConfigTTool.VCDPath);
}
public static void setBasicConfig(boolean systemcOn) {
......@@ -286,7 +286,7 @@ public class SpecConfigTTool {
try {
Element elt = (Element) (nl.item(0));
lastVCD = elt.getAttribute("data");
ExternalCommand1 = "gtkwave " + lastVCD;
// ExternalCommand1 = "gtkwave " + lastVCD;
} catch (Exception e) {
throw new MalformedConfigurationException(e.getMessage());
}
......
......@@ -58,10 +58,10 @@ public class TraceManager {
public static int devPolicy = TO_CONSOLE;
public static int errPolicy = TO_CONSOLE;
public static void addDev(String _s) {
public static void addDev(String res) {
switch(devPolicy) {
case TO_CONSOLE:
System.out.println(_s);
System.out.println(res);
break;
case TO_DEVNULL:
break;
......
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
......@@ -91,7 +91,7 @@ public class ActivityDiagram2TMLTranslator {
TMLActivity activity = tmltask.getActivityDiagram();
TMLActivityDiagramPanel tadp = (TMLActivityDiagramPanel)(activity.getReferenceObject());
TraceManager.addDev( "Generating activity diagram of: " + tmltask.getName());
//TraceManager.addDev( "Generating activity diagram of: " + tmltask.getName());
// search for start state
List<TGComponent> list = tadp.getComponentList();
......
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
......@@ -1921,7 +1921,7 @@ public class AvatarDesignPanelTranslator {
final AvatarSMDConnector connector ) {
final AvatarStateMachineOwner block = transition.getBlock();
final AvatarSpecification spec = block.getAvatarSpecification();
final String probabilityStr = modifyString( connector.getEffectiveProbability() );
final String probabilityStr = connector.getEffectiveProbability() ;
final int error = AvatarSyntaxChecker.isAValidProbabilityExpr( spec, block, probabilityStr );
if ( error < 0 ) {
......@@ -1929,6 +1929,7 @@ public class AvatarDesignPanelTranslator {
}
if ( probabilityStr != null && !probabilityStr.isEmpty() ) {
//TraceManager.addDev("Probability=" + probabilityStr);
transition.setProbability( Double.parseDouble( probabilityStr ) );
}
}
......
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
......@@ -139,6 +139,7 @@ import java.util.List;
// AVATAR
// AVATAR
//Communication Pattern javaCC parser
//Communication Pattern javaCC parser
//import compiler.tmlCPparser.*;
......@@ -201,8 +202,10 @@ public class GTURTLEModeling {
private String tlsa;
private String tlsadot;
private List<SimulationTrace> simulationTraces;
private List<RG> graphs;
private GraphTree gt;
private SimulationTraceTree stt;
private int nbRTLOTOS;
private int nbSuggestedDesign;
......@@ -264,6 +267,7 @@ public class GTURTLEModeling {
pointerOperation = -1;
graphs = new ArrayList<RG>();
simulationTraces = new ArrayList<SimulationTrace>();
invariants = new LinkedList<Invariant>();
//vdt = new ValidationDataTree(mgui);
......@@ -271,6 +275,7 @@ public class GTURTLEModeling {
idt = new InvariantDataTree(mgui);
st = new SearchTree(mgui);
gt = new GraphTree(mgui);
stt = new SimulationTraceTree(mgui);
/*if (!Charset.isSupported("UTF-8")) {
ErrorGUI.exit(ErrorGUI.ERROR_CHARSET);
......@@ -290,6 +295,36 @@ public class GTURTLEModeling {
return tm.isARegularTIFSpec();
}
public List<SimulationTrace> getSimulationTraces() {
return simulationTraces;
}
public void addSimulationTrace(SimulationTrace newTrace) {
//TraceManager.addDev("Adding new simulation trace " + newTrace);
if (newTrace.hasFile()) {
// We have to remove identical traces
LinkedList<SimulationTrace> ll = new LinkedList<>();
for(SimulationTrace trace: simulationTraces) {
if (trace.hasFile()) {
if (trace.getFullPath().compareTo(newTrace.getFullPath()) == 0) {
ll.add(trace);
}
}
}
for(SimulationTrace trace: ll) {
simulationTraces.remove(trace);
}
}
simulationTraces.add(newTrace);
}
public void removeSimulationTrace(SimulationTrace oldTrace) {
//TraceManager.addDev("Adding new graph " + newGraph);
simulationTraces.remove(oldTrace);
}
public List<RG> getRGs() {
return graphs;
}
......@@ -2582,6 +2617,22 @@ public class GTURTLEModeling {
mgui.dtree.expandMyPath(new TreePath(obj));
mgui.dtree.forceUpdate();
} else {
TraceManager.addDev("Pb to expand Graph tree");
}
}
public void expandToSimulationTraces() {
if ((stt != null) && (simulationTraces != null) && (simulationTraces.size() > 0)) {
Object[] obj = new Object[2];
obj[0] = mgui.dtree.getModel().getRoot();
obj[1] = stt;
TraceManager.addDev("Expanding Path because of simulation traces");
mgui.dtree.expandMyPath(new TreePath(obj));
mgui.dtree.forceUpdate();
} else {
TraceManager.addDev("Pb to expand ST tree");
}
}
......@@ -2590,7 +2641,7 @@ public class GTURTLEModeling {
}
public int getChildCount() {
return panels.size() + 4;
return panels.size() + 5;
}
public Object getChild(int index) {
......@@ -2599,8 +2650,10 @@ public class GTURTLEModeling {
} else if (index == panels.size()) {
return mcvdt;
} else if (index == (panels.size() + 1)) {
return gt;
return stt;
} else if (index == (panels.size() + 2)) {
return gt;
} else if (index == (panels.size() + 3)) {
return idt;
} else {
return st;
......@@ -2618,16 +2671,20 @@ public class GTURTLEModeling {
return panels.size();
}
if (child == gt) {
if (child == stt) {
return panels.size() + 1;
}
if (child == idt) {
if (child == gt) {
return panels.size() + 2;
}
if (child == idt) {
return panels.size() + 3;
}
return panels.size() + 3;
return panels.size() + 4;
}
// Projection management
......
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
......@@ -769,6 +769,35 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
jfm.setVisible(true);
}
// Simulation traces
public List<SimulationTrace> getSimulationTraces() {
return gtm.getSimulationTraces();
}
public void addSimulationTrace(SimulationTrace _newSimulationTrace) {
gtm.addSimulationTrace(_newSimulationTrace);
expandToSimulationTraces();
dtree.toBeUpdated();
}
public void removeSimulationTrace(SimulationTrace _toBeRemoved) {
gtm.removeSimulationTrace(_toBeRemoved);
/*if (_toBeRemoved.fileName != null) {
TraceManager.addDev("Filename=" + _toBeRemoved.fileName);
File toBeDeleted = new File(_toBeRemoved.fileName);
try {
toBeDeleted.delete();
TraceManager.addDev("File of RG was deleted on disk");
} catch (Exception e) {
}
}*/
dtree.toBeUpdated();
}
public void showInFinder(RG inputGraph) {
TraceManager.addDev("in show in finder");
if (inputGraph.fileName == null) {
......@@ -789,6 +818,32 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
// Can open directory or file
public void showInFinder(SimulationTrace trace, boolean openDirectory) {
TraceManager.addDev("in show in finder");
if (!trace.hasFile()) {
return;
}
if (!Desktop.isDesktopSupported()) {
return;
}
File file = new File(trace.getFullPath());
if (openDirectory) {
if (!file.isDirectory()) {
file = file.getParentFile();
}
}
TraceManager.addDev("Getting desktop");
Desktop desktop = Desktop.getDesktop();
try {
TraceManager.addDev("Opening in desktop");
desktop.open(file);
} catch (Exception e) {
TraceManager.addDev("Exception in opening explorer: " + e.getMessage());
}
}
public void setCurrentInvariant(Invariant inv) {
currentInvariant = inv;
}
......@@ -1174,6 +1229,12 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
}
public void expandToSimulationTraces() {
if (gtm != null) {
gtm.expandToSimulationTraces();
}
}
public Vector<String> getTMLTasks() {
TURTLEPanel tp;
Vector<String> list = new Vector<String>();
......@@ -2783,7 +2844,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
FileOutputStream fos = new FileOutputStream(libfile);
fos.write(data.getBytes());
fos.close();
JOptionPane.showMessageDialog(frame, "Modeling was correctly saved under a TURTLE library named " + libfile.getName(), "Saving", JOptionPane.INFORMATION_MESSAGE);
JOptionPane.showMessageDialog(frame, "Modeling was correctly saved under a TTool library named " + libfile.getName(), "Saving", JOptionPane.INFORMATION_MESSAGE);
return;
} catch (Exception e) {
JOptionPane.showMessageDialog(frame, "File could not be saved because " + e.getMessage(), "File Error", JOptionPane.INFORMATION_MESSAGE);
......@@ -5611,6 +5672,10 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
public void runGTKWave(String pathToFile) {
executeUserCommand("localhost", ConfigurationTTool.GTKWavePath + " " + pathToFile);
}
public void showModifiedAUTDOT() {
String s = GTURTLEModeling.runDOTTY(modifiedautdot);
if (s != null) {
......
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
*
* ludovic.apvrille AT telecom-paristech.fr
*
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards their
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
package ui;
public class SimulationTrace {
private String name;
private String fullPathToFile = null;
private int type;
public static final int VCD_DIPLO = 0;
public static final int TXT_DIPLO = 1;
public static final int HTML_DIPLO = 2;
public static final int PNG_AVATAR = 3;
public static final int TXT_AVATAR = 4;
public static final int SVG_AVATAR = 5;
private static String[] TYPES = {"VCD DIPLO", "TXT DIPLO", "HTML DIPLO", "PNG AVATAR", "TXT AVATAR", "SVG AVATAR"};
public SimulationTrace(String name, int type) {
this(name, type, null);
}
public SimulationTrace(String name, int type, String fullPathToFile) {
this.name = name;
this.type = type;
this.fullPathToFile = fullPathToFile;
}
public int getType() {
return type;
}
public String getTypeString() {
return TYPES[type];
}
public String getFullPath() {
return fullPathToFile;
}
public String getToolTip() {
return "Simulation trace. Name:" + name;
}
public boolean hasFile() {
return fullPathToFile != null;
}
public String getName() {
return name;
}
public String toString() {
String ret="";
ret += name + " of type " + TYPES[type];
if (fullPathToFile != null) {
ret += " " + fullPathToFile;
}
return ret;
}
}
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
This diff is collapsed.
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.