diff --git a/src/main/java/recipe/analysis/ToNuXmv.java b/src/main/java/recipe/analysis/ToNuXmv.java index 8309786..fc66aba 100644 --- a/src/main/java/recipe/analysis/ToNuXmv.java +++ b/src/main/java/recipe/analysis/ToNuXmv.java @@ -562,118 +562,122 @@ else if (receiveGuardExpr.toString().equals("FALSE")) { Map> receiveAgentReceivePreds = new HashMap<>(); Map> receiveAgentReceiveProgressConds = new HashMap<>(); - for (State receiveAgentState : receiveAgent.getStates()) { - Set receiveAgentReceiveTransitions = agentStateReceiveTransitionMap.get(receiveAgent).get(receiveAgentState); - if(receiveAgentReceiveTransitions == null){ - receiveAgentReceiveTransitions = new HashSet<>(); - } - String receiveStateIsCurrentState = receiveName + "-automaton-state" + " = " + receiveAgentState.toString(); - - List transitionReceivePreds = new ArrayList<>(); - List transitionReceiveProgressConds = new ArrayList<>(); - - receiveTransLoop: - for (Transition receiveTrans : receiveAgentReceiveTransitions) { - ReceiveProcess receiveProcess = (ReceiveProcess) receiveTrans.getLabel(); - - List receiveTransTriggeredIf = new ArrayList<>(); - List receiveTransEffects = new ArrayList<>(); - - //This is a hack to allow us to stop considering this transition - // when the incoming message does not contain all message vars required - // for this transition - AtomicReference stop = new AtomicReference(false); - Function stopHelper = (e) -> { - stop.set(true); - return e; - }; - - // relabel the transition guard - // for message vars with the relabelled sending Agent messages and - // for local vars with the name of the agent - Expression receiveTransitionGuard = receiveProcess.getPsi() - .relabel(v -> sendingProcess.getMessage().containsKey(((TypedVariable) v).getName()) - ? relabelledMessage.get(((TypedVariable) v).getName()) - : (system.getMessageStructure().containsKey(((TypedVariable) v).getName()) - ? stopHelper.apply(v) - : ((TypedVariable) v).sameTypeWithName(receiveName + "-" + v))); - receiveTransitionGuard = receiveTransitionGuard.simplify(); - - ////stop considering this transition if the incoming message does not contain all message vars required - if (stop.get()) continue receiveTransLoop; - //////////////////////// - - // if the receiveTransitionGuard has evaluated to false, then we can stop. - if (receiveTransitionGuard.equals(Condition.getFalse())) - continue receiveTransLoop; - else - receiveTransTriggeredIf.add(receiveTransitionGuard.toString()); - - - Expression receivingOnThisChannelVarOrVal = receiveProcess.getChannel() - .relabel(v -> v.sameTypeWithName(receiveName + "-" + v.toString())); - - // if the sending and receiving transition channels are both values, - // and they are not the same values then this transition can stop being - // considered - if (receivingOnThisChannelVarOrVal.getClass().equals(TypedValue.class) - && sendingOnThisChannelVarOrVal.getClass().equals(TypedValue.class) - && !sendingOnThisChannelVarOrVal.equals(receivingOnThisChannelVarOrVal)) - continue receiveTransLoop; - else - receiveTransTriggeredIf.add(sendingOnThisChannelVarOrVal + " = " + receivingOnThisChannelVarOrVal); -// agentReceiveNows.add(receiveNow); - //for each variable update, if the updates uses a message variable that is - // not set by the send transition, then exit - // else relabel variables appropriately - for (Map.Entry entry : receiveProcess.getUpdate().entrySet()) { - receiveTransEffects - .add("next(" + receiveName + "-" + entry.getKey() + ") = (" - + entry.getValue().relabel(v -> - sendingProcess.getMessage().containsKey(((TypedVariable) v).getName()) - ? relabelledMessage.get(((TypedVariable) v).getName()) - : (system.getMessageStructure().containsKey(((TypedVariable) v).getName()) - ? stopHelper.apply((TypedVariable) v) - : ((TypedVariable) v).sameTypeWithName(receiveName + "-" + v))) + ")"); + if (!sendGuardExprHere.toString().equals("FALSE")) { + for (State receiveAgentState : receiveAgent.getStates()) { + Set receiveAgentReceiveTransitions = agentStateReceiveTransitionMap.get(receiveAgent).get(receiveAgentState); + if (receiveAgentReceiveTransitions == null) { + receiveAgentReceiveTransitions = new HashSet<>(); } - //stop considering this transition if update uses a message variable - // that is not set by the send transition - if (stop.get()) continue receiveTransLoop; - /////// + String receiveStateIsCurrentState = receiveName + "-automaton-state" + " = " + receiveAgentState.toString(); + + List transitionReceivePreds = new ArrayList<>(); + List transitionReceiveProgressConds = new ArrayList<>(); + + receiveTransLoop: + for (Transition receiveTrans : receiveAgentReceiveTransitions) { + ReceiveProcess receiveProcess = (ReceiveProcess) receiveTrans.getLabel(); + + List receiveTransTriggeredIf = new ArrayList<>(); + List receiveTransEffects = new ArrayList<>(); + + //This is a hack to allow us to stop considering this transition + // when the incoming message does not contain all message vars required + // for this transition + AtomicReference stop = new AtomicReference(false); + Function stopHelper = (e) -> { + stop.set(true); + return e; + }; + + // relabel the transition guard + // for message vars with the relabelled sending Agent messages and + // for local vars with the name of the agent + Expression receiveTransitionGuard = receiveProcess.getPsi() + .relabel(v -> sendingProcess.getMessage().containsKey(((TypedVariable) v).getName()) + ? relabelledMessage.get(((TypedVariable) v).getName()) + : (system.getMessageStructure().containsKey(((TypedVariable) v).getName()) + ? stopHelper.apply(v) + : ((TypedVariable) v).sameTypeWithName(receiveName + "-" + v))); + receiveTransitionGuard = receiveTransitionGuard.simplify(); + + ////stop considering this transition if the incoming message does not contain all message vars required + if (stop.get()) continue receiveTransLoop; + //////////////////////// + + // if the receiveTransitionGuard has evaluated to false, then we can stop. + if (receiveTransitionGuard.equals(Condition.getFalse())) + continue receiveTransLoop; + else + receiveTransTriggeredIf.add(receiveTransitionGuard.toString()); + + + Expression receivingOnThisChannelVarOrVal = receiveProcess.getChannel() + .relabel(v -> v.sameTypeWithName(receiveName + "-" + v.toString())); + + // if the sending and receiving transition channels are both values, + // and they are not the same values then this transition can stop being + // considered + if (receivingOnThisChannelVarOrVal.getClass().equals(TypedValue.class) + && sendingOnThisChannelVarOrVal.getClass().equals(TypedValue.class) + && !sendingOnThisChannelVarOrVal.equals(receivingOnThisChannelVarOrVal)) + continue receiveTransLoop; + else + receiveTransTriggeredIf.add(sendingOnThisChannelVarOrVal + " = " + receivingOnThisChannelVarOrVal); + // agentReceiveNows.add(receiveNow); + + //for each variable update, if the updates uses a message variable that is + // not set by the send transition, then exit + // else relabel variables appropriately + for (Map.Entry entry : receiveProcess.getUpdate().entrySet()) { + receiveTransEffects + .add("next(" + receiveName + "-" + entry.getKey() + ") = (" + + entry.getValue().relabel(v -> + sendingProcess.getMessage().containsKey(((TypedVariable) v).getName()) + ? relabelledMessage.get(((TypedVariable) v).getName()) + : (system.getMessageStructure().containsKey(((TypedVariable) v).getName()) + ? stopHelper.apply((TypedVariable) v) + : ((TypedVariable) v).sameTypeWithName(receiveName + "-" + v))) + ")"); + } - // keep the same variables for variables not mentioned in the update - for (String var : receiveAgent.getStore().getAttributes().keySet()) { - if (!receiveProcess.getUpdate().containsKey(var)) { - receiveTransEffects.add("next(" + receiveName + "-" + var + ") = " + receiveName + "-" + var); + //stop considering this transition if update uses a message variable + // that is not set by the send transition + if (stop.get()) continue receiveTransLoop; + /////// + + // keep the same variables for variables not mentioned in the update + for (String var : receiveAgent.getStore().getAttributes().keySet()) { + if (!receiveProcess.getUpdate().containsKey(var)) { + receiveTransEffects.add("next(" + receiveName + "-" + var + ") = " + receiveName + "-" + var); + } } - } - //if the receive transition is labelled, then set it's next value as true - // and set all other labels of this agents as false - if (receiveProcess.getLabel() != null && !receiveProcess.getLabel().equals("")) { - receiveTransEffects.add("next(" + receiveName + "-" + receiveProcess.getLabel() + ") = TRUE"); - receiveTransEffects.add("falsify-not-" + receiveName + "-" + receiveProcess.getLabel() + ""); - } else { - // if the transition is not labelled, then when it is taken no label - // should be set as true - receiveTransEffects.add("falsify-not-" + receiveName); - } + //if the receive transition is labelled, then set it's next value as true + // and set all other labels of this agents as false + if (receiveProcess.getLabel() != null && !receiveProcess.getLabel().equals("")) { + receiveTransEffects.add("next(" + receiveName + "-" + receiveProcess.getLabel() + ") = TRUE"); + receiveTransEffects.add("falsify-not-" + receiveName + "-" + receiveProcess.getLabel() + ""); + } else { + // if the transition is not labelled, then when it is taken no label + // should be set as true + receiveTransEffects.add("falsify-not-" + receiveName); + } - // set the transition destination state as the next state - receiveTransEffects.add("next(" + receiveName + "-automaton-state" + ") = " + receiveTrans.getDestination()); + // set the transition destination state as the next state + receiveTransEffects.add("next(" + receiveName + "-automaton-state" + ") = " + receiveTrans.getDestination()); - transitionReceivePreds.add("(" + String.join(")\n \t\t& (", receiveTransTriggeredIf) + ") & " - + "(" + String.join(")\n \t\t& (", receiveTransEffects) + ")"); + transitionReceivePreds.add("(" + String.join(")\n \t\t& (", receiveTransTriggeredIf) + ") & " + + "(" + String.join(")\n \t\t& (", receiveTransEffects) + ")"); - transitionReceiveProgressConds.add("(" + String.join(")\n \t\t& (", receiveTransTriggeredIf) + ")"); - } + transitionReceiveProgressConds.add("(" + String.join(")\n \t\t& (", receiveTransTriggeredIf) + ")"); + } - if(transitionReceivePreds.size() > 0) { - receiveAgentReceivePreds.put(receiveStateIsCurrentState, transitionReceivePreds); - receiveAgentReceiveProgressConds.put(receiveStateIsCurrentState, transitionReceiveProgressConds); + if (transitionReceivePreds.size() > 0) { + receiveAgentReceivePreds.put(receiveStateIsCurrentState, transitionReceivePreds); + receiveAgentReceiveProgressConds.put(receiveStateIsCurrentState, transitionReceiveProgressConds); + } } } @@ -704,8 +708,7 @@ else if (receiveGuardExpr.toString().equals("FALSE")) { //This checks that the receive guard holds, the transition relation holds, and the send guard holds // otherwise a disjunct is not added to the above lists if (receiveAgentReceivePreds.size() > 0 - && !receiveGuard.equals("FALSE") - && !sendGuardExprHere.toString().equals("FALSE")) { + && !receiveGuard.equals("FALSE")) { //Compute transition predicate (and progress predicate) for current agent List stateTransitionPreds = new ArrayList<>(); List stateTransitionProgressConds = new ArrayList<>();