/* * To change this template, choose Tools | Templates * and open the template in the editor. */ package RULES; import CREATOR_CONDICTIONS_RULES.CreatorBinaryRules; import CSP_CREATOR.CreatorNewComponent; import CSP_CREATOR.CreatorTypesAndChannels; import LOGIC.BoolType; import LOGIC.Channel; import LOGIC.Contract; import LOGIC.Instance; import LOGIC.ObjectList; import LOGIC.Componente; import LOGIC.Datatype; import LOGIC.IntervalType; import LOGIC.Protocols; import LOGIC.Type; import java.io.File; import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; import java.util.LinkedList; /** * * @author forall */ public class CreatorRuleInterleaveComposition { private LinkedList instance; private String rule = ""; private Contract c; private Componente component; //private CreatorNewComponent newcomp;//o novo componente está sendo criado na interface private String novoComponente = ""; private CreatorTypesAndChannels typechannels; public CreatorRuleInterleaveComposition(LinkedList i, ObjectList lt) { instance = i; //rule = new CreatorBinaryRules(i, lt); c = new Contract(); c.setName("RuleInterleaveOf" + i.get(0).getName() + "_" + i.get(1).getName()); typechannels = new CreatorTypesAndChannels(lt); typechannels.creatorTypesChannels(); novoComponente = i.get(0).getName() + "_" + i.get(1).getName(); } public void creatorRule() { int cont = 0; //rule.creatorCSP(); rule = rule + "include \"sequence_aux.csp\" \ninclude \"function_aux.csp\" \n" + "include \"auxiliar.csp\" \ninclude \"rules.csp\""; rule = rule + "\n\n"; rule = rule + typechannels.getTypeChannel(); //não preciso de types e channels de contrato, pois estou declarando todos os tipos e canais do ObjectList //no caso, todo canal q eu criar vai possuir algum tipo e canal dessa lista. rule = rule + "\n\n"; int st1 = instance.get(0).getContrato().getBehavior().indexOf("="); int st2 = instance.get(1).getContrato().getBehavior().indexOf("="); String s1 = instance.get(0).getContrato().getBehavior().substring(0, st1 - 1); String s2 = instance.get(0).getContrato().getBehavior().substring(0, st2 - 1); if (instance.get(0).getContrato().getBehavior().equals(instance.get(1).getContrato().getBehavior())) { rule = rule + "\n" + instance.get(0).getContrato().getBehavior() + "\n"; }else if(s1.equals(s2)){ // se o nome dos processos forem iguais pego o maior //pois tem um comportamento a mais especificado nele if(instance.get(0).getContrato().getBehavior().length() > instance.get(1).getContrato().getBehavior().length()){ rule = rule + "\n" + instance.get(0).getContrato().getBehavior() + "\n"; }else{ rule = rule + "\n" + instance.get(1).getContrato().getBehavior() + "\n"; } }else if(instance.get(0).getContrato().getBehavior().contains(instance.get(1).getContrato().getBehavior())){ rule = rule + "\n" + instance.get(0).getContrato().getBehavior() + "\n"; }else if(instance.get(1).getContrato().getBehavior().contains(instance.get(0).getContrato().getBehavior())){ rule = rule + "\n" + instance.get(1).getContrato().getBehavior() + "\n"; } else { rule = rule + "\n" + instance.get(0).getContrato().getBehavior() + "\n" + "\n\n"+ instance.get(1).getContrato().getBehavior() + "\n"; } rule = rule + "\n\n"; creatorRenameFunction(); creatorChannelFunction(); creatorInputFunction(); creatorOutputFunction(); rule = rule + "\n\n"; rule = rule + "--INTERLEAVING COMPOSITION"; rule = rule + " \n" + novoComponente + " = INTER("; for (Instance instance1 : instance) {// para cada objeto pertencente a lista instance, execute o que est[a logo a baixo } if (cont == instance.size() - 1) { rule = rule + instance1.getName(); } else { rule = rule + instance1.getName() + ","; } cont++; } rule = rule + ") "; rule = rule + "\nassert STOP [T= RUN(inter(events(" + instance.get(0).getName() + "),events(" + instance.get(1).getName() + ")))"; rule = rule + "\nassert " + novoComponente + ":[deadlock free[FD]]"; salvarArquivoCSP(); } private void salvarArquivoCSP() { FileWriter compInter = null; try { c.setName("RuleInterleaveOf" + instance.get(0).getName() + "_" + instance.get(1).getName()); compInter = new FileWriter(new File("cspFiles/" + c.getName() + ".csp")); PrintWriter p = new PrintWriter(compInter); p.flush(); //System.out.println(rule); p.write(rule); compInter.close(); p.close(); } catch (IOException ex) { //Logger.getLogger(instance.getName()).log(Level.SEVERE, null, ex); System.out.println("Ocorreu um problena na manipulação de arquivo"); } } private void creatorRenameFunction() { rule = rule + "\n\n"; for (Instance instance1 : instance) { //c = instance1.getContrato(); rule = rule + "Inst_" + instance1.getName() + " = <"; for (int i = 0; i < instance1.getChannel().size(); i++) { if (i == instance1.getChannel().size() - 1) { rule = rule + "(" + instance1.getContrato().getChannel().get(i).getName() + "," + instance1.getChannel().get(i).getName() + ")"; } else { rule = rule + "(" + instance1.getContrato().getChannel().get(i).getName() + "," + instance1.getChannel().get(i).getName() + "),"; // System.out.println("Canais do contrato da instancia:" + // instance1.getContrato().getChannel()); } } rule = rule + "> \n"; rule = rule + instance1.getName() + " = rename(" + instance1.getContrato().getName() + ", Inst_" + instance1.getName() + ") \n\n"; } } private void creatorChannelFunction() { // CHANNELS int cont = 0; //channels rule = rule + "\nGET_CHANNELS(P) ="; rule = rule + "\n \t let f ="; rule = rule + "\n \t < \n"; for (Instance instance1 : instance) { rule = rule + "\t(" + instance1.getName() + ", { "; for (int j = 0; j < instance1.getChannel().size(); j++) { if (j == instance1.getChannel().size() - 1) { rule = rule + instance1.getChannel().get(j).getName(); } else { rule = rule + instance1.getChannel().get(j).getName() + ","; } } cont++; if (cont == instance.size() - 1) { rule = rule + " }),"; rule = rule + "\n"; } else { rule = rule + " })"; rule = rule + "\n"; } rule = rule + "\n"; } rule = rule + " \t > \n"; rule = rule + "\n \t within apply(f,P )"; } private void creatorInputFunction() { int cont = 0; //função inputs rule = rule + "\n"; // verificação para o contrato rule = rule + "\ninputs( P ) = "; rule = rule + "\n \t let f = \n\t<"; for (Instance instance1 : instance) {// para cada objeto pertencente a lista inst, execute o que est[a logo a baixo rule = rule + "\n \t ( " + instance1.getName() + ", {| "; // coloca todos os canais de in associado com seus tipos. ex: {|c.1, c.2|} for (int i = 0; i < instance1.getIn().size(); i++) { if (i == instance1.getIn().size() - 1) { rule = rule + instance1.getIn().get(i).getEvento(); } else { rule = rule + instance1.getIn().get(i).getEvento() + ","; } } if (cont == instance.size() - 1) { rule = rule + " |})"; } else { rule = rule + " |}),"; } cont++; } rule = rule + "\n \t > \n"; rule = rule + "\n \t within apply(f, P )"; } private void creatorOutputFunction() { int cont = 0; //função outputs rule = rule + "\n outputs( P ) = "; rule = rule + "\n \t let f =\n\t < "; for (Instance instance1 : instance) {// para cada objeto pertencente a lista inst, execute o que est[a logo a baixo rule = rule + "\n\t ( " + instance1.getName() + ", {| "; // coloca todos os canais de out associado com seus tipos. ex: {|c.1, c.2|} for (int i = 0; i < instance1.getOut().size(); i++) { if (i == instance1.getOut().size() - 1) { rule = rule + instance1.getOut().get(i).getEvento(); } else { rule = rule + instance1.getOut().get(i).getEvento() + ","; } } if (cont == instance.size() - 1) { rule = rule + " |})"; } else { rule = rule + " |}),"; } cont++; } rule = rule + "\n \t >"; rule = rule + "\n \t within apply(f, P )"; } private String channelCompleteForm(Channel channel) { //recebe um canal e retorna ele no tipo "canal.tipo.tipo..." String retorno = ""; retorno = channel.getName() + "."; for (int i = 0; i < channel.getType().size(); i++) { if (i == channel.getType().size() - 1) { retorno = retorno + channel.getType().get(i).getNome(); } else { retorno = retorno + channel.getType().get(i).getNome() + "."; } } return retorno; } public void typeInstanciation(Type tipo) { if (tipo instanceof BoolType) { rule = rule + "\n" + tipo.getNome() + " = Bool"; } // verificando se 'tipo é do tipo 'IntervalType if (tipo instanceof IntervalType) { //instanciando interval IntervalType interval = (IntervalType) tipo; rule = rule + "\n" + tipo.getNome() + " = {" + interval.getMim() + ".." + interval.getMax() + "}"; } if (tipo instanceof Datatype) { rule = rule + "\n" + "datatype " + tipo.getNome() + " = "; //instanciando Datatype Datatype datatype = (Datatype) tipo; int j; for (j = 0; j < datatype.getDatatype().size(); j++) { if (j != 0) { rule = rule + " | "; } if (!datatype.getDatatype().get(j).getType().equals("")) { rule = rule + datatype.getDatatype().get(j).getName() + "." + datatype.getDatatype().get(j).getType(); } else { rule = rule + datatype.getDatatype().get(j).getName(); } } } } private void channelInstanciation(Channel Canal) { rule = rule + "\nchannel " + Canal.getName() + " : "; for (int i = 0; i < Canal.getType().size(); i++) { if (i == Canal.getType().size() - 1) { rule = rule + Canal.getType().get(i).getNome(); } else { rule = rule + Canal.getType().get(i).getNome() + "."; } } } }