/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package CSP_ANALYSE;
import CREATOR_CONDICTIONS_RULES.CreatorNamesOfProcessCSP;
import CREATOR_CONDICTIONS_RULES.CreatorProtocol;
import LOGIC.Barra;
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 AnalyseRuleCommunication {
private ArrayList<FDRResult> rule1;//i/oconfluente c1
private ArrayList<FDRResult> rule2;//i/oconfluente c2
private ArrayList<FDRResult> rule3;//protocolo compatível c1
private ArrayList<FDRResult> rule4;//protocolo compatível c2
private ArrayList<FDRResult> rule5;//have infinite traces
private ArrayList<FDRResult> ruleResult;
private LinkedList<Instance> instance;
private String pegarErro = "";
private Contract c;
private ReadFileCSP rdf;
private ReturnMensageFDR mensagemF;
private LinkedList<Protocols> prot;
private CreatorNamesOfProcessCSP creatName;
private LinkedList<String> colocaprot;
private LinkedList<String> colocaprot_RIO;
private LinkedList<String> colocaDual_prot_RIO;
private String eventoprotocol1 = "";
private String eventoprotocol2 = "";
private Barra barra;
public AnalyseRuleCommunication(LinkedList<Instance> i, LinkedList<Protocols> p) throws InterruptedException {
instance = i;
rule1 = new ArrayList<FDRResult>();
rule2 = new ArrayList<FDRResult>();
rule3 = new ArrayList<FDRResult>();
rule4 = new ArrayList<FDRResult>();
rule5 = new ArrayList<FDRResult>();
ruleResult = new ArrayList<FDRResult>();
barra = new Barra();
barra.criarBarra(5);
c = new Contract();
c.setName("RuleCommunicationOf" + i.get(0).getName() + "_" + i.get(1).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<>();
//pegando o nome do evento que passei por paramentro no protocolo
int pr1, pr2, pr3, pr4;
pr1 = p.get(0).getProtocol().indexOf("(");
pr2 = p.get(0).getProtocol().lastIndexOf(")");
eventoprotocol1 = p.get(0).getProtocol().substring(pr1 + 1, pr2);
pr3 = p.get(1).getProtocol().indexOf("(");
pr4 = p.get(1).getProtocol().lastIndexOf(")");
eventoprotocol2 = p.get(1).getProtocol().substring(pr3 + 1, pr4);
}
public ArrayList<FDRResult> 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()
+ " \\ {|" + eventoprotocol1
+ "|} [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 STOP [T= RUN(inter(events("
+ instance.get(0).getName() + "),events("
+ instance.get(1).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("The Alphabets are disjont");
retorno.setResultado(true);
rule1.add(retorno);
} else {
retorno.setMensagem("The Alphabets aren't disjont");
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() + ","
+ eventoprotocol1 + ")")) {
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() + ","
+ eventoprotocol1
+ ") [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()
+ "," + eventoprotocol1 + "),{|"
+ eventoprotocol1
+ "|})) [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()
+ "," + eventoprotocol1 + "),{|"
+ eventoprotocol1
+ "|})) [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) + ","
+ eventoprotocol1 + ") :[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);
}
}
barra.aumentar(line);
// verifcando I/O confluente para componente 2
//componente 2
//Checking Cell1\{|rd1|} [T= Cell1
} else if (line.equals("Checking " + instance.get(1).getName()
+ " \\ {|" + prot.get(1).getCanal().getName()
+ "|} [T= " + instance.get(1).getName())) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
rule2.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);
rule2.add(retorno);
} else {
retorno.setMensagem("NOT");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking " + colocaprot.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);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking " + colocaprot.get(1)
+ " [F= PROT_IMP_def("
+ instance.get(1).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);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking PROT_IMP_def("
+ instance.get(1).getName() + ","
+ prot.get(1).getCanal().getName()
+ ") [FD= " + colocaprot.get(1))) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking Test(subseteq(inputs_PROT_IMP("
+ instance.get(1).getName()
+ "," + prot.get(1).getCanal().getName()
+ "),{|" + 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);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking Test(subseteq(outputs_PROT_IMP("
+ instance.get(1).getName()
+ "," + prot.get(1).getCanal().getName() + "),{|"
+ 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);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
} else if (line.equals("Checking InBufferProt(" + colocaprot_RIO.get(1)
+ "," + eventoprotocol2 + ") :[deterministic [F]]")) {
line = pegarResultado.readLine();
if (line == null) {
FDRResult retorno = new FDRResult();
retorno.setMensagem("O arquivo CSP está com erro");
retorno.setResultado(false);
rule2.add(retorno);
} else {
FDRResult retorno = new FDRResult();
if (line.equals("true") || line.equals("xtrue")) {
retorno.setMensagem("YES");
retorno.setResultado(true);
rule2.add(retorno);
} else {
retorno.setMensagem("NO");
retorno.setResultado(false);
rule2.add(retorno);
}
}
barra.aumentar(line);
//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) + "), {| "
+ eventoprotocol1 + "|})) [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) + "), {|"
+ eventoprotocol2 + "|})) [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);
}
}
barra.aumentar(line);
} 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);
}
}
barra.aumentar(line);
// 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);
}
}
}
barra.aumentar(line);
}
} catch (Exception e) {
e.printStackTrace();
JOptionPane.showMessageDialog(null, "error occurred in verifying the composition");
}
ruleResult.add(pegaSaídaR1(rule1));
ruleResult.add(pegaSaídaR2(rule2));
ruleResult.add(pegaSaídaR3(rule3));
ruleResult.add(pegaSaídaR4(rule4));
ruleResult.add(pegaSaídaR5(rule5));
ruleResult.add(mensagemF.returnMensagefdr());
for (int i = 0; i < ruleResult.size(); i++) {
System.out.println(ruleResult.get(i).getMensagem());
System.out.println(ruleResult.get(i).getResultado());
}
barra.finalizar();
return ruleResult;
}
//I/O confluence
private FDRResult pegaSaídaR1(ArrayList<FDRResult> r) {
FDRResult result = new FDRResult();
if (r.size() == 0) {
result.setResultado(false);
result.setMensagem("O arquivo CSP está com erro");
return result;
} else {
for (int i = 0; i < r.size(); i++) {
if (r.get(i).getResultado() == false) {
result.setMensagem("The protocol implementation on "
+ eventoprotocol1
+ "\n of the " + instance.get(0).getName()
+ " is not a valid I/O Confluent");
result.setResultado(false);
return result;
}
}
}
result.setMensagem("The protocol implementation on "
+ eventoprotocol1
+ "\n of the " + instance.get(0).getName()
+ " is a valid I/O Confluent");
result.setResultado(true);
return result;
}
private FDRResult pegaSaídaR2(ArrayList<FDRResult> r) {
FDRResult result = new FDRResult();
if (r.size() == 0) {
result.setResultado(false);
result.setMensagem("O arquivo CSP está com erro");
return result;
} else {
for (int i = 0; i < r.size(); i++) {
if (r.get(i).getResultado() == false) {
result.setMensagem("The protocol implementation on "
+ eventoprotocol2
+ "\n of the " + instance.get(1).getName()
+ " is not a valid I/O Confluent");
result.setResultado(false);
return result;
}
}
}
result.setMensagem("The protocol implementation on "
+ eventoprotocol2
+ "\n of the " + instance.get(1).getName()
+ " is a valid I/O Confluent");
result.setResultado(true);
return result;
}
private FDRResult pegaSaídaR3(ArrayList<FDRResult> r) {
FDRResult result = new FDRResult();
if (r.size() == 0) {
result.setResultado(false);
result.setMensagem("O arquivo CSP está com erro");
return result;
} else {
for (int i = 0; i < r.size(); i++) {
if (r.get(i).getResultado() == false) {
result.setMensagem("Protocols of "
+ instance.get(0).getName()
+ "\n aren't strongly compatible in "
+ eventoprotocol1);
result.setResultado(false);
return result;
}
}
}
result.setMensagem("Protocols of "
+ instance.get(0).getName()
+ "\n are strongly compatible in "
+ eventoprotocol1);
result.setResultado(true);
return result;
}
private FDRResult pegaSaídaR4(ArrayList<FDRResult> r) {
FDRResult result = new FDRResult();
if (r.size() == 0) {
result.setResultado(false);
result.setMensagem("O arquivo CSP está com erro");
return result;
} else {
for (int i = 0; i < r.size(); i++) {
if (r.get(i).getResultado() == false) {
result.setMensagem("Protocols of "
+ instance.get(1).getName()
+ "\n aren't strongly compatible in "
+ eventoprotocol2);
result.setResultado(false);
return result;
}
}
}
result.setMensagem("Protocols of "
+ instance.get(1).getName()
+ " are strongly compatible in "
+ eventoprotocol2);
result.setResultado(true);
return result;
}
private FDRResult pegaSaídaR5(ArrayList<FDRResult> r) {
FDRResult result = new FDRResult();
if (r.size() == 0) {
result.setResultado(false);
result.setMensagem("O arquivo CSP está com erro");
return result;
} else {
for (int i = 0; i < r.size(); i++) {
if (r.get(i).getResultado() == false) {
result.setMensagem("Protocols don't have finite output property");
result.setResultado(false);
return result;
}
}
}
result.setMensagem("Protocols have finite output property");
result.setResultado(true);
return result;
}
}
/*
System.out.println("Analyse\n\n\n");
System.out.println("Checking " + instance.get(0).getName() +
"\\{|" + instance.get(0).getChannel().get(0).getName() +
"|} [T= " + instance.get(0));
System.out.println("\n\n");
System.out.println("Checking STOP [T= RUN(inter(events(" +
instance.get(0).getName() + "),events(" +
instance.get(1).getName() + ")))");
System.out.println("\n\n");
System.out.println("Checking" + colocaprot.get(0)+
" :[divergence free [FD]]");
System.out.println("\n\n");
System.out.println("Checking" + colocaprot.get(0)+ " [F= PROT_IMP_def("
+ instance.get(0).getName() + "," + prot.get(0).getCanal().getName() + ")");
System.out.println("\n\n");
System.out.println("Checking PROT_IMP_def(" + instance.get(0).getName() + ","
+ prot.get(0).getCanal().getName()
+ ") [FD= " + colocaprot.get(0));
System.out.println("\n\n");
System.out.println("Checking PROT_IMP_def(" + instance.get(0).getName() + ","
+ prot.get(0).getCanal().getName()
+ ") [FD= " + colocaprot.get(0));
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" +
instance.get(0).getName()
+ ","+prot.get(0).getCanal().getName() + "),{|" +
prot.get(0).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" +
instance.get(0).getName()
+ ","+prot.get(0).getCanal().getName() + "),{|" +
prot.get(0).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(outputs_PROT_IMP("
+ instance.get(0).getName()
+ ","+prot.get(0).getCanal().getName() + "),{|" +
prot.get(0).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(outputs_PROT_IMP("
+ instance.get(0).getName()
+ ","+prot.get(0).getCanal().getName() + "),{|" +
prot.get(0).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " +
prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
System.out.println("\n\n");
System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " +
prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
System.out.println("\n\n");
System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(0) + ", " +
prot.get(0).getCanal().getName() + ") :[deterministic [F]]");
System.out.println("\n\n");
System.out.println("Checking" + colocaprot.get(1)+ " [F= PROT_IMP_def("
+ instance.get(1).getName() + "," + prot.get(1).getCanal().getName() + ")");
System.out.println("\n\n");
System.out.println("Checking PROT_IMP_def(" + instance.get(1).getName() + ","
+ prot.get(1).getCanal().getName()
+ ") [FD= " + colocaprot.get(1));
System.out.println("\n\n");
System.out.println("Checking PROT_IMP_def(" + instance.get(1).getName() + ","
+ prot.get(1).getCanal().getName()
+ ") [FD= " + colocaprot.get(1));
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs_PROT_IMP(" +
instance.get(1).getName()
+ ","+prot.get(1).getCanal().getName() + "),{|" +
prot.get(1).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(outputs_PROT_IMP("
+ instance.get(1).getName()
+ ","+prot.get(1).getCanal().getName() + "),{|" +
prot.get(1).getCanal().getName()
+ "|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking InBufferProt(" + colocaprot_RIO.get(1) + ", " +
prot.get(1).getCanal().getName() + ") :[deterministic [F]]");
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(0) + " :[deadlock free [FD]]");
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(1) + " :[deadlock free [FD]]");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs("+
colocaprot_RIO.get(0) + "),{|" + prot.get(0).getCanal().getName() +
"|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(outputs("+
colocaprot_RIO.get(0) + "),{|" + prot.get(1).getCanal().getName() +
"|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs("+
colocaprot_RIO.get(1) + "),{|" + prot.get(1).getCanal().getName() +
"|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(inputs("+
colocaprot_RIO.get(1) + "),{|" + prot.get(1).getCanal().getName() +
"|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(subseteq(outputs("+
colocaprot_RIO.get(1) + "),{|" + prot.get(0).getCanal().getName() +
"|})) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(inputs("+
colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
+ ")) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(inputs("+
colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
+ ")) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(inputs("+
colocaprot_RIO.get(0) + " == outputs(" + colocaDual_prot_RIO.get(0)
+ ")) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(outputs("+
colocaprot_RIO.get(1) + " == inputs(" + colocaDual_prot_RIO.get(1)
+ ")) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking Test(outputs("+
colocaprot_RIO.get(1) + " == inputs(" + colocaDual_prot_RIO.get(1)
+ ")) [T= ERROR");
System.out.println("\n\n");
System.out.println("Checking "+
colocaDual_prot_RIO.get(0) + " [T= " + colocaprot_RIO.get(0));
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(0) + " [T= " + colocaDual_prot_RIO.get(0));
System.out.println("\n\n");
System.out.println("Checking "+
colocaDual_prot_RIO.get(0) + " [F= " + colocaprot_RIO.get(1));
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(1) + " [T= " + colocaDual_prot_RIO.get(0));
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(0) + "\\outputs(" + colocaprot_RIO.get(0) +
" :[divergence free [FD]]");
System.out.println("\n\n");
System.out.println("Checking "+
colocaprot_RIO.get(1) + "\\outputs(" + colocaprot_RIO.get(1) +
" :[divergence free [FD]]");
*/