/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package CSP_ANALYSE;
import CSP_CREATOR.CreatorContract;
import CSP_CREATOR.CreatorInstance;
import LOGIC.Contract;
import LOGIC.Instance;
import LOGIC.ObjectList;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.InputStreamReader;
import java.util.ArrayList;
import javax.swing.JOptionPane;
/**
*
* @author forall
*/
public class AnalyseFDR {
private Contract contract;
private ArrayList<FDRResult> resultadoFDR;
private ArrayList<FDRResult> strongOutputDChannel;
private CreatorContract creatC;
private CreatorInstance creatI;
private String strongOchannel = "";
private ReadFileCSP readF;
private ReturnMensageFDR mensagemFdr;
public AnalyseFDR(Contract c, ObjectList l) {
contract = c;
resultadoFDR = new ArrayList<>();
strongOutputDChannel = new ArrayList<>();
creatC = new CreatorContract(c, l);
readF = new ReadFileCSP(c);
mensagemFdr = new ReturnMensageFDR(c);
}
public ArrayList<FDRResult> takeResultIOProcess() {
readF.saidaFDR();
// vai ler o arquivo saidaFDR.log verificando as condições de IOProcess
File pegarSaida = new File("fdrLog/"+contract.getName()+"_saida_"+readF.getTemp()+".log");
if (!pegarSaida.exists()) {
System.exit(-1);
}
try {
BufferedReader pegarResultado = new BufferedReader(new FileReader(pegarSaida));
String line = "";
while ((line = pegarResultado.readLine()) != null) {
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
resultadoFDR.add(retorno);
} else if (line.equals("Checking Test(inter(inputs(" + contract.getName() + "),outputs(" + contract.getName() + ")) == {}) [T= ERROR")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
resultadoFDR.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("Contract's Channels are I/O Channel");
retorno.setResultado(true);
resultadoFDR.add(retorno);
} else {
retorno.setMensagem("Contract's Channels aren't I/O Channel");
retorno.setResultado(false);
resultadoFDR.add(retorno);
}
}
} else if (line.equals("Checking HideAll(" + contract.getName() + ") :[divergence free [FD]]")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
resultadoFDR.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("The Contract's behavior has Infinite Traces");
retorno.setResultado(true);
resultadoFDR.add(retorno);
} else {
retorno.setMensagem("The Contract's behavior doesn't have Infinite Traces");
retorno.setResultado(false);
resultadoFDR.add(retorno);
}
}
} else if (line.equals("Checking " + contract.getName() + " :[divergence free [FD]]")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
resultadoFDR.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("The Contract's behavior is Divergence Free");
retorno.setResultado(true);
resultadoFDR.add(retorno);
} else {
retorno.setMensagem("The Contract's behavior isn't Divergence Free");
retorno.setResultado(false);
resultadoFDR.add(retorno);
}
}
} else if (line.equals("Checking LHS_InputDet(" + contract.getName() + ") [F= RHS_InputDet(" + contract.getName() + ")")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
resultadoFDR.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("The Contract's behavior is input Deterministic");
retorno.setResultado(true);
resultadoFDR.add(retorno);
} else {
retorno.setMensagem("The Contract's behavior isn't input Deterministic");
retorno.setResultado(false);
resultadoFDR.add(retorno);
}
}
} else if (line.equals("Checking LHS_OutputDec_A(" + contract.getName() + ") [F= RHS_OutputDec_A(" + contract.getName() + ")")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult r = new FDRResult();
r.setMensagem("O arquivo CSP está com erro");
r.setResultado(false);
strongOutputDChannel.add(r);
} else {
FDRResult r = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
r.setMensagem("The Contract's behavior is output decisive");
r.setResultado(true);
strongOutputDChannel.add(r);
} else {
r.setMensagem("The Contract's behavior isn't output decisive");
r.setResultado(false);
strongOutputDChannel.add(r);
}
}
} else if (line.contains("Checking LHS_OutputDec_B(")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult r = new FDRResult();
r.setMensagem("O arquivo CSP está com erro");
r.setResultado(false);
strongOutputDChannel.add(r);
} else {
FDRResult r = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
r.setMensagem("The Contract is output decisive in channels");
r.setResultado(true);
strongOutputDChannel.add(r);
} else {
r.setMensagem("The Contract NOT is output decisive in channels");
r.setResultado(false);
strongOutputDChannel.add(r);
}
}
}
}
} catch (Exception e) {
e.printStackTrace();
JOptionPane.showMessageDialog(null, "error occurred in checking IO / Process");
}
resultadoFDR.add(StrongOutputIsTrue());
//returnMensagefdr();
resultadoFDR.add(mensagemFdr.returnMensagefdr());
return resultadoFDR;
}
public FDRResult StrongOutputIsTrue() {
FDRResult retorno = new FDRResult();
for (int i = 0; i < strongOutputDChannel.size(); i++) {
if ((!strongOutputDChannel.get(i).getResultado())) {
retorno.setMensagem("The Contract is NOT output decisive");
retorno.setResultado(false);
//resultadoFDR.add(retorno);
} else {
retorno.setMensagem("The Contract is output decisive");
retorno.setResultado(true);
//resultadoFDR.add(retorno);
}
}
//retorna o resultado do strongOutputDecisiviness
return retorno;
}
}