/*
* 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> 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<Instance> 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() + ".";
}
}
}
}