workcraft/XmasPlugin/src/org/workcraft/plugins/xmas/tools/XmasVerificationTool.java
package org.workcraft.plugins.xmas.tools;
import org.workcraft.commands.Command;
import org.workcraft.dom.Node;
import org.workcraft.gui.tools.AbstractGraphEditorTool;
import org.workcraft.gui.tools.Decorator;
import org.workcraft.gui.tools.GraphEditor;
import org.workcraft.interop.ExternalProcess;
import org.workcraft.plugins.xmas.VisualXmas;
import org.workcraft.plugins.xmas.Xmas;
import org.workcraft.plugins.xmas.XmasSettings;
import org.workcraft.plugins.xmas.components.QueueComponent;
import org.workcraft.plugins.xmas.components.SyncComponent;
import org.workcraft.plugins.xmas.components.VisualQueueComponent;
import org.workcraft.plugins.xmas.components.VisualSyncComponent;
import org.workcraft.plugins.xmas.gui.SolutionsDialog1;
import org.workcraft.plugins.xmas.gui.SolutionsDialog2;
import org.workcraft.utils.DialogUtils;
import org.workcraft.utils.FileUtils;
import org.workcraft.utils.LogUtils;
import org.workcraft.utils.WorkspaceUtils;
import org.workcraft.workspace.WorkspaceEntry;
import java.awt.*;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;
public class XmasVerificationTool extends AbstractGraphEditorTool implements Command {
@Override
public String getSection() {
return "Verification";
}
@Override
public String getDisplayName() {
return "Verification";
}
private static class Qslist {
public final String name;
public final int chk;
Qslist(String s1, int n) {
name = s1;
chk = n;
}
}
private static String level = "";
private static String display = "";
private static String highlight = "";
private static final List<Qslist> qslist = new ArrayList<>();
private static List<String> processArg(String file) {
Scanner sc = null;
try {
sc = new Scanner(new File(file));
} catch (FileNotFoundException e) {
LogUtils.logError(e.getMessage());
}
String targ = "";
String larg = "";
String sarg = "";
while (sc.hasNextLine()) {
Scanner line = new Scanner(sc.nextLine());
Scanner nxt = new Scanner(line.next());
String check = nxt.next();
String str;
if (check.startsWith("trace")) {
nxt = new Scanner(line.next());
targ = "-t";
targ += nxt.next();
} else if (check.startsWith("level")) {
nxt = new Scanner(line.next());
larg = "-v";
str = nxt.next();
level = str;
if ("normal".equals(str)) {
//System.out.println("Read v1");
larg = "-v1";
} else if ("advanced".equals(str)) {
//System.out.println("Read v2");
larg = "-v2";
}
} else if (check.startsWith("display")) {
nxt = new Scanner(line.next());
str = nxt.next();
//System.out.println("strrr=" + str);
display = str;
} else if (check.startsWith("highlight")) {
nxt = new Scanner(line.next());
str = nxt.next();
//System.out.println("strrr=" + str);
highlight = str;
} else if (check.startsWith("soln")) {
nxt = new Scanner(line.next());
str = nxt.next();
//System.out.println("solnnnnnnnnnnnnnnnnn=" + str);
sarg = "-s" + str;
}
}
ArrayList<String> args = new ArrayList<>();
if (!targ.isEmpty()) args.add(targ);
if (!larg.isEmpty()) args.add(larg);
if (!sarg.isEmpty()) args.add(sarg);
return args;
}
private static String processLoc(String file) {
Scanner sc = null;
try {
sc = new Scanner(new File(file));
} catch (FileNotFoundException e) {
LogUtils.logError(e.getMessage());
}
String str = "";
while (sc.hasNextLine()) {
String line = sc.nextLine();
//System.out.println(sc.next());
str += line + '\n';
}
return str;
}
private static void processQsl(String file) {
qslist.clear();
Scanner sc = null;
try {
sc = new Scanner(new File(file));
} catch (FileNotFoundException e) {
LogUtils.logError(e.getMessage());
}
while (sc.hasNextLine()) {
Scanner line = new Scanner(sc.nextLine());
Scanner nxt = new Scanner(line.next());
String check = nxt.next();
nxt = new Scanner(line.next());
String str = nxt.next();
int num = Integer.parseInt(str);
//System.out.println("qsl " + check + ' ' + str + ' ' + num);
qslist.add(new Qslist(check, num));
}
}
private static String processEq(String file) {
Scanner sc = null;
try {
sc = new Scanner(new File(file));
} catch (FileNotFoundException e) {
LogUtils.logError(e.getMessage());
}
String str = "";
while (sc.hasNextLine()) {
String line = sc.nextLine();
//System.out.println(sc.next());
str += line + '\n';
}
return str;
}
public int checkType(String s) {
if (s.contains("DEADLOCK FREE")) {
return 0;
} else if (s.contains("TRACE FOUND")) {
return 1;
} else if (s.contains("Local")) {
return 2;
}
return -1;
}
public void initHighlight(Xmas xnet, VisualXmas vnet) {
VisualQueueComponent vqc;
VisualSyncComponent vsc;
for (Node node : vnet.getNodes()) {
if (node instanceof VisualQueueComponent) {
vqc = (VisualQueueComponent) node;
vqc.setForegroundColor(Color.BLACK);
} else if (node instanceof VisualSyncComponent) {
vsc = (VisualSyncComponent) node;
vsc.setForegroundColor(Color.BLACK);
}
}
}
public void localHighlight(String s, Xmas xnet, VisualXmas vnet) {
QueueComponent qc;
SyncComponent sc;
VisualQueueComponent vqc;
VisualSyncComponent vsc;
//System.out.println("s=" + s);
for (String st : s.split(" |\n")) {
if (st.startsWith("Q") || st.startsWith("S")) {
System.out.println(st);
for (Node node : vnet.getNodes()) {
if (node instanceof VisualQueueComponent) {
vqc = (VisualQueueComponent) node;
qc = vqc.getReferencedComponent();
//if (xnet.getName(qc).contains(st)) {
String rstr;
rstr = xnet.getName(qc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(st)) {
vqc.setForegroundColor(Color.RED);
}
} else if (node instanceof VisualSyncComponent) {
vsc = (VisualSyncComponent) node;
sc = vsc.getReferencedComponent();
//if (xnet.getName(qc).contains(st)) {
String rstr;
rstr = xnet.getName(sc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(st)) {
vsc.setForegroundColor(Color.RED);
}
}
}
}
}
}
public void relHighlight(String s, Xmas xnet, VisualXmas vnet) {
int typ = 0;
String str = "";
QueueComponent qc;
SyncComponent sc;
VisualQueueComponent vqc;
VisualSyncComponent vsc;
for (String st : s.split(" |;|\n")) {
//if (st.startsWith("Q")) {
if (st.contains("->")) {
//System.out.println("testst" + st);
typ = 0;
for (String st2 : st.split("->")) {
str = st2;
//System.out.println("str===" + str);
for (Node node : vnet.getNodes()) {
if (node instanceof VisualQueueComponent) {
vqc = (VisualQueueComponent) node;
qc = vqc.getReferencedComponent();
//System.out.println("x===" + xnet.getName(qc));
String rstr;
rstr = xnet.getName(qc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(str) && typ == 0) {
vqc.setForegroundColor(Color.PINK);
}
} else if (node instanceof VisualSyncComponent) {
vsc = (VisualSyncComponent) node;
sc = vsc.getReferencedComponent();
//System.out.println("strrr===" + str + ' ' + xnet.getName(sc));
String rstr;
rstr = xnet.getName(sc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(str) && typ == 0) {
vsc.setForegroundColor(Color.PINK);
}
}
}
}
} else if (st.contains("<-")) {
//System.out.println("testst_" + st);
typ = 1;
for (String st2 : st.split("<-")) {
str = st2;
//System.out.println("str===" + str);
for (Node node : vnet.getNodes()) {
if (node instanceof VisualQueueComponent) {
vqc = (VisualQueueComponent) node;
qc = vqc.getReferencedComponent();
String rstr;
rstr = xnet.getName(qc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(str) && (typ == 1)) {
vqc.setForegroundColor(Color.RED);
}
} else if (node instanceof VisualSyncComponent) {
vsc = (VisualSyncComponent) node;
sc = vsc.getReferencedComponent();
String rstr;
rstr = xnet.getName(sc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(str) && (typ == 1)) {
vsc.setForegroundColor(Color.RED);
}
}
}
}
}
//}
}
}
public void activeHighlight(Xmas xnet, VisualXmas vnet) {
QueueComponent qc;
SyncComponent sc;
VisualQueueComponent vqc;
VisualSyncComponent vsc;
for (Qslist ql : qslist) {
if (ql.chk == 0) {
for (Node node : vnet.getNodes()) {
if (node instanceof VisualQueueComponent) {
vqc = (VisualQueueComponent) node;
qc = vqc.getReferencedComponent();
String rstr;
rstr = xnet.getName(qc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(ql.name)) {
vqc.setForegroundColor(Color.GREEN);
}
} else if (node instanceof VisualSyncComponent) {
vsc = (VisualSyncComponent) node;
sc = vsc.getReferencedComponent();
String rstr;
rstr = xnet.getName(sc);
rstr = rstr.replace(rstr.charAt(0), Character.toUpperCase(rstr.charAt(0)));
if (rstr.equals(ql.name)) {
vsc.setForegroundColor(Color.GREEN);
}
}
}
}
}
}
@Override
public boolean isApplicableTo(WorkspaceEntry we) {
return WorkspaceUtils.isApplicable(we, Xmas.class);
}
@Override
public void run(WorkspaceEntry we) {
System.out.println("Verifying Model");
final VisualXmas vnet = WorkspaceUtils.getAs(we, VisualXmas.class);
final Xmas xnet = WorkspaceUtils.getAs(we, Xmas.class);
try {
File cpnFile = XmasSettings.getTempVxmCpnFile();
File inFile = XmasSettings.getTempVxmInFile();
FileUtils.copyFile(cpnFile, inFile);
ArrayList<String> vxmCommand = new ArrayList<>();
vxmCommand.add(XmasSettings.getTempVxmCommandFile().getAbsolutePath());
vxmCommand.addAll(processArg(XmasSettings.getTempVxmVsettingsFile().getAbsolutePath()));
ExternalProcess.printCommandLine(vxmCommand);
String[] cmdArray = vxmCommand.toArray(new String[vxmCommand.size()]);
Process vxmProcess = Runtime.getRuntime().exec(cmdArray, null, XmasSettings.getTempVxmDirectory());
String s;
String str = "";
InputStreamReader inputStreamReader = new InputStreamReader(vxmProcess.getInputStream());
BufferedReader stdInput = new BufferedReader(inputStreamReader);
int n = 0;
int test = -1;
initHighlight(xnet, vnet);
while ((s = stdInput.readLine()) != null) {
if (test == -1) test = checkType(s);
if (n > 0) str += s + '\n';
n++;
System.out.println(s);
}
if ("advanced".equals(level)) {
System.out.println("LEVEL IS ADVANCED ");
File qslFile = XmasSettings.getTempVxmQslFile();
processQsl(qslFile.getAbsolutePath());
File equFile = XmasSettings.getTempVxmEquFile();
str = processEq(equFile.getAbsolutePath());
} else if ("normal".equals(level) && (test == 2)) {
System.out.println("LEVEL IS NORMAL ");
File locFile = XmasSettings.getTempVxmLocFile();
str = processLoc(locFile.getAbsolutePath());
}
if (test > 0) {
if ("popup".equals(display)) {
if ("advanced".equals(level)) {
new SolutionsDialog2(test, str);
} else {
new SolutionsDialog1(test, str);
}
}
if (test == 2) {
if ("local".equals(highlight)) {
localHighlight(str, xnet, vnet);
} else if ("rel".equals(highlight)) {
relHighlight(str, xnet, vnet);
//System.out.println("str = " + str);
activeHighlight(xnet, vnet);
}
}
} else if (test == 0) {
if ("popup".equals(display)) {
DialogUtils.showInfo("The system is deadlock-free.");
}
}
} catch (Exception e) {
e.printStackTrace();
}
}
@Override
public String getLabel() {
return null;
}
@Override
public Decorator getDecorator(GraphEditor editor) {
return null;
}
}