/* * To change this template, choose Tools | Templates * and open the template in the editor. */ package CSP_ANALYSE; import CREATOR_CONDICTIONS_RULES.CreatorNamesOfProcessCSP; import LOGIC.Contract; import LOGIC.Instance; import LOGIC.Protocols; import java.io.BufferedReader; import java.io.File; import java.io.FileReader; import java.util.ArrayList; import java.util.LinkedList; import javax.swing.JOptionPane; /** * * @author sarah */ public class AnalyseRuleFeedback { private ArrayList rule1;//i/oconfluente c1 private ArrayList rule2;//i/oconfluente c2 private ArrayList rule3;//protocolo compatível c1 private ArrayList rule4;//protocolo compatível c2 private ArrayList rule5;//have infinite traces private ArrayList ruleResult; private LinkedList instance; private String pegarErro = ""; private Contract c; private ReadFileCSP rdf; private ReturnMensageFDR mensagemF; private LinkedList prot; private CreatorNamesOfProcessCSP creatName; private LinkedList colocaprot; private LinkedList colocaprot_RIO; private LinkedList colocaDual_prot_RIO; public AnalyseRuleFeedback(LinkedList i, LinkedList p) { instance = i; rule1 = new ArrayList(); rule2 = new ArrayList(); rule3 = new ArrayList(); rule4 = new ArrayList(); rule5 = new ArrayList(); ruleResult = new ArrayList(); c = new Contract(); c.setName("RuleFeedbackOf" + i.get(0).getName() + "_" + i.get(0).getName()); rdf = new ReadFileCSP(c); mensagemF = new ReturnMensageFDR(c); prot = p; creatName = new CreatorNamesOfProcessCSP(i, p); colocaprot = new LinkedList<>(); colocaprot_RIO = new LinkedList<>(); colocaDual_prot_RIO = new LinkedList<>(); } public ArrayList resultRule() { colocaprot = creatName.CreatorProt_Name(); colocaprot_RIO = creatName.CreatorProt_RIO(); colocaDual_prot_RIO = creatName.CreatorDual_Prot_RIO(); rdf.saidaFDR(); // vai ler o arquivo saidaFDR.log verificando as condições de IOProcess File pegarSaida = new File("fdrLog/" + c.getName() + "_saida_" + rdf.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); ruleResult.add(retorno); //Checking Cell0\{|rd0|} [T= Cell0 } else if (line.equals("Checking " + instance.get(0).getName() + " \\ {|" + prot.get(0).getCanal().getName() + "|} [T= " + instance.get(0).getName())) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("channel is in the alphabet of contract"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NOT"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking " + colocaprot.get(0) + " :[divergence free [FD]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking " + colocaprot.get(0) + " [F= PROT_IMP_def(" + instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + ")")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking PROT_IMP_def(" + instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + ") [FD= " + colocaprot.get(0))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking Test(subseteq(inputs_PROT_IMP(" + instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + "),{|" + prot.get(0).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking Test(subseteq(outputs_PROT_IMP(" + instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + "),{|" + prot.get(0).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } } else if (line.equals("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " + prot.get(0).getCanal().getName() + ") :[deterministic [F]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule1.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule1.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule1.add(retorno); } } //outro conjunto de verificações //D.6: Protocols are Strong Compatible //componente 1 } else if (line.equals("Checking " + colocaprot_RIO.get(0) + " :[deadlock free [FD]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking Test(subseteq(inputs(" + colocaprot_RIO.get(0) + "), {| " + prot.get(0).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking Test(subseteq(outputs(" + colocaprot_RIO.get(0) + "), {|" + prot.get(1).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking Test(inputs(" + colocaprot_RIO.get(0) + ") == outputs(" + colocaDual_prot_RIO.get(0) + ")) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking Test(outputs(" + colocaprot_RIO.get(0) + ") == inputs(" + colocaDual_prot_RIO.get(0) + ")) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking " + colocaDual_prot_RIO.get(0) + " [T= " + colocaprot_RIO.get(0))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking " + colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking " + colocaDual_prot_RIO.get(0) + " [F= " + colocaprot_RIO.get(1))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } } else if (line.equals("Checking " + colocaprot_RIO.get(1) + " [F= " + colocaDual_prot_RIO.get(0))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule3.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule3.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule3.add(retorno); } } //protocolo fortemente compatível //componente 2 } else if (line.equals("Checking " + colocaprot_RIO.get(1) + " :[deadlock free [FD]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking Test(subseteq(inputs(" + colocaprot_RIO.get(1) + "), {| " + prot.get(1).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking Test(subseteq(outputs(" + colocaprot_RIO.get(1) + "), {| " + prot.get(0).getCanal().getName() + "|})) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking Test(inputs(" + colocaprot_RIO.get(1) + ") == outputs(" + colocaDual_prot_RIO.get(1) + ")) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking Test(outputs(" + colocaprot_RIO.get(1) + ") == inputs(" + colocaDual_prot_RIO.get(1) + ")) [T= ERROR")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking " + colocaDual_prot_RIO.get(1) + " [T= " + colocaprot_RIO.get(1))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking " + colocaprot_RIO.get(1) + " [T= " + colocaDual_prot_RIO.get(1))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking " + colocaDual_prot_RIO.get(1) + " [F= " + colocaprot_RIO.get(0))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking " + colocaprot_RIO.get(0) + " [F= " + colocaDual_prot_RIO.get(1))) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } // outro conjunto de verificações // Protocols have finite output property } else if (line.equals("Checking " + colocaprot_RIO.get(0) + " \\ outputs(" + colocaprot_RIO.get(0) + "):[divergence free [FD]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule5.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule5.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule5.add(retorno); } } } else if (line.equals("Checking " + colocaprot_RIO.get(1) + " \\ outputs(" + colocaprot_RIO.get(1) + "):[divergence free [FD]]")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule5.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule5.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule5.add(retorno); } } // verificando se canais são desacoplados }else if (line.equals("Checking INTER_PROT_IMP(" + colocaprot.get(0) + ", {" + prot.get(0).getCanal().getName() + ", " + prot.get(1).getCanal().getName() + "}) [F= PROJECTION(" + instance.get(0).getName() + ", {" + prot.get(0).getCanal().getName() + ", " + prot.get(1).getCanal().getName() + "})")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } else if (line.equals("Checking PROJECTION(" + instance.get(0).getName() + ", {" + prot.get(0).getCanal().getName() + ", " + prot.get(1).getCanal().getName() + "}) [FD= INTER_PROT_IMP(" + colocaprot.get(0) + ", {" + prot.get(0).getCanal().getName() + ", " + prot.get(1).getCanal().getName() + "})")) { line = pegarResultado.readLine(); if (line == null) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); rule4.add(retorno); } else { FDRResult retorno = new FDRResult(); if (line.equals("true") || line.equals("xtrue")) { retorno.setMensagem("YES"); retorno.setResultado(true); rule4.add(retorno); } else { retorno.setMensagem("NO"); retorno.setResultado(false); rule4.add(retorno); } } } } } catch (Exception e) { e.printStackTrace(); JOptionPane.showMessageDialog(null, "error occurred in verifying the composition"); } //colocar em ruleResult o que será emviado para a interface //primeira lista boolean b1 = pegaSaída(rule1); if(b1){ FDRResult retorno = new FDRResult(); retorno.setMensagem("The protocol implementation on " + prot.get(0).getCanal().getName() + " of the" + instance.get(0).getName() + " is valid and I/O Confluent"); retorno.setResultado(true); ruleResult.add(retorno); }else{ FDRResult retorno = new FDRResult(); retorno.setMensagem("The protocol is NOT implementation on " + prot.get(0).getCanal().getName() + " of the" + instance.get(0).getName() + " is valid and I/O Confluent"); retorno.setResultado(false); ruleResult.add(retorno); } //protocolos compatíveis // terceira boolean b3 = pegaSaída(rule3); if(b3){ FDRResult retorno = new FDRResult(); retorno.setMensagem("Protocols of " + instance.get(0).getName() + " is strong compatible in " + prot.get(0).getCanal().getName()); retorno.setResultado(true); ruleResult.add(retorno); }else{ FDRResult retorno = new FDRResult(); retorno.setMensagem("Protocols of " + instance.get(0).getName() + " aren't strong compatible in " + prot.get(0).getCanal().getName()); retorno.setResultado(false); ruleResult.add(retorno); } //quinta lista //have infinite propert boolean b5 = pegaSaída(rule5); if(b5){ FDRResult retorno = new FDRResult(); retorno.setMensagem("Protocols have finite output property"); retorno.setResultado(true); ruleResult.add(retorno); }else{ FDRResult retorno = new FDRResult(); retorno.setMensagem("Protocols don't have finite output property"); retorno.setResultado(false); ruleResult.add(retorno); } boolean b6 = pegaSaída(rule4); if(b6){ FDRResult retorno = new FDRResult(); retorno.setMensagem("The componente is desacopled channels"); retorno.setResultado(true); ruleResult.add(retorno); }else{ FDRResult retorno = new FDRResult(); retorno.setMensagem("The componente don't desacopled channels"); retorno.setResultado(false); ruleResult.add(retorno); } //pegarErroSaida(); if (ruleResult.size() == 0) { FDRResult retorno = new FDRResult(); retorno.setMensagem("O arquivo CSP está com erro"); retorno.setResultado(false); ruleResult.add(retorno); } for(int i = 0; i< ruleResult.size(); i++){ System.out.println(ruleResult.get(i).getMensagem()); System.out.println(ruleResult.get(i).getResultado()); } ruleResult.add(mensagemF.returnMensagefdr()); return ruleResult; } private boolean pegaSaída(ArrayList r) { for (int i = 0; i < r.size(); i++) { if (r.get(i).getResultado() == false) { return false; } } return true; } }