From 0e22810aae06870857402ea2b14e7947ffd23b83 Mon Sep 17 00:00:00 2001 From: davidebasile Date: Thu, 30 Nov 2023 20:53:02 +0100 Subject: [PATCH] implemented TauActions, and committed states. The CompositionFunction has been updated to use committed states, as well as ignore modalities. This is useful for model checking, to use the properties to specify the behaviour of the automaton in a top-down way. The converter now also reads committed states. CALabel has been updated. There are also some temporary attempts, classes that probably will be removed in the future, like HideNecessaryModality.java and DkBricsEncoder.java Signed-off-by: Davide Basile --- .../catlib/automaton/Automaton.java | 21 ++ .../catlib/automaton/label/CALabel.java | 60 +++- .../automaton/label/action/TauAction.java | 66 ++++ .../catlib/automaton/state/AbstractState.java | 1 + .../catlib/automaton/state/BasicState.java | 19 + .../automaton/transition/ModalTransition.java | 9 +- .../catlib/converters/AutConverter.java | 2 + .../catlib/converters/AutDataConverter.java | 36 +- .../operations/CompositionFunction.java | 79 +++-- .../operations/ModelCheckingFunction.java | 23 +- .../ModelCheckingSynthesisOperator.java | 95 +++-- .../NewOrchestrationSynthesisOperator.java | 330 ++++++++++++------ .../operations/RemovePrincipalOperator.java | 73 ++++ .../catlib/requirements/StrongAgreement.java | 6 +- .../catlib/toignore/DkBricsEncoder.java | 125 +++++++ .../toignore/HideNecessaryModality.java | 87 +++++ .../catlib/automaton/AutomatonTest.java | 6 +- .../catlib/family/FMCATest.java | 6 + .../catlib/automaton/ITAutomatonTest.java | 2 + .../encoders/ITDkBricksEncoderTest.java | 67 ++++ .../operators/ITNewOrchestrationTest.java | 112 +++++- src/test/resources/(AxB).data | 1 + .../(BusinessClientxHotelxEconomyClient).data | 1 + .../BusinessClientxHotelxEconomyClient.data | 1 + ...nessClientxHotelxEconomyClient_export.data | 1 + src/test/resources/Dealer.data | 27 +- src/test/resources/DealerNoCommitted.data | 23 ++ .../NewOrc_(DealerxPlayerxPlayer).data | 101 +++--- ...Orc_(DealerxPlayerxPlayer)_modelcheck.data | 135 +++++++ src/test/resources/PlayerEncoded.data | 19 + .../testcor_concur21_Example34_closureCA.data | 1 + 31 files changed, 1288 insertions(+), 247 deletions(-) create mode 100644 src/main/java/io/github/contractautomata/catlib/automaton/label/action/TauAction.java create mode 100644 src/main/java/io/github/contractautomata/catlib/operations/RemovePrincipalOperator.java create mode 100644 src/main/java/io/github/contractautomata/catlib/toignore/DkBricsEncoder.java create mode 100644 src/main/java/io/github/contractautomata/catlib/toignore/HideNecessaryModality.java create mode 100644 src/test/java/it/io/github/contractautomata/catlib/encoders/ITDkBricksEncoderTest.java create mode 100644 src/test/resources/DealerNoCommitted.data create mode 100644 src/test/resources/NewOrc_(DealerxPlayerxPlayer)_modelcheck.data create mode 100644 src/test/resources/PlayerEncoded.data diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/Automaton.java b/src/main/java/io/github/contractautomata/catlib/automaton/Automaton.java index 306defe5..de0e495d 100644 --- a/src/main/java/io/github/contractautomata/catlib/automaton/Automaton.java +++ b/src/main/java/io/github/contractautomata/catlib/automaton/Automaton.java @@ -176,10 +176,31 @@ public String toString() { .sorted() .toArray())); pr.append("]").append(System.lineSeparator()); + pr.append("Committed states: ["); + for (int i=0;i pr.append(t).append(System.lineSeparator())); return pr.toString(); } + + /** + * true if the automaton is determistic, false otherwise + * + * @return true if the automaton is determistic, false otherwise + */ + public boolean isDeterministic(){ + return this.getTransition().parallelStream() + .noneMatch(t->this.getTransition().parallelStream() + .filter(tt->tt!=t) + .noneMatch(tt->t.getSource().equals(tt.getSource()) && t.getLabel().equals(tt.getLabel()))); + } } \ No newline at end of file diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/label/CALabel.java b/src/main/java/io/github/contractautomata/catlib/automaton/label/CALabel.java index ea6a08a1..b5c715d9 100644 --- a/src/main/java/io/github/contractautomata/catlib/automaton/label/CALabel.java +++ b/src/main/java/io/github/contractautomata/catlib/automaton/label/CALabel.java @@ -7,6 +7,7 @@ import java.util.stream.IntStream; /** + * * Class implementing a label of a Contract Automaton, by extending the super class Label.
* The content of each label is a list of actions.
* Contract automata labels can be of three types:
@@ -52,10 +53,11 @@ public CALabel(List label) { super(label); - if (label.stream().anyMatch(l->!(l instanceof OfferAction)&&!(l instanceof RequestAction)&&!(l instanceof IdleAction)) || + if (label.stream().anyMatch(l->!(l instanceof OfferAction)&&!(l instanceof RequestAction)&&!(l instanceof IdleAction)&&!(l instanceof TauAction)) || label.stream().allMatch(IdleAction.class::isInstance) || label.stream().filter(OfferAction.class::isInstance).count()>1 || - label.stream().filter(RequestAction.class::isInstance).count()>1) + label.stream().filter(RequestAction.class::isInstance).count()>1 || + label.stream().filter(TauAction.class::isInstance).count()>1) throw new IllegalArgumentException("The label is not well-formed"); } @@ -85,6 +87,20 @@ private Integer getRequesterIfAny() { .findAny().orElse(-1); } + + /** + * Returns the index of the principal performing the tau action, or -1 in + * case no principal is performing a tau move + * @return the index of the principal performing the tau action, or -1 in + * case no principal is performing a tau move. + */ + private Integer getTauMoverIfAny() { + List label = this.getContent(); + return IntStream.range(0, label.size()) + .filter(i->label.get(i) instanceof TauAction) + .findAny().orElse(-1); + } + /** * Returns the index of the principal performing the offer action. * There must be a principal performing an offer action. @@ -113,6 +129,22 @@ public Integer getRequester() { else return requester; } + + /** + * Returns the index of the principal performing the tau action. + * There must be a principal performing a tau action. + * + * @return the index of the principal performing the tau action. + * There must be a principal performing a tau action. + */ + public Integer getTauMover() { + Integer taumover = getTauMoverIfAny(); + if (taumover ==-1) throw new UnsupportedOperationException(); + else return taumover; + } + + + /** * Returns true if the action is a match * @return true if the action is a match @@ -129,7 +161,7 @@ public boolean isMatch() */ public boolean isOffer() { - return getRequesterIfAny() == -1; + return !this.isTau() && getRequesterIfAny() == -1; } @@ -139,7 +171,17 @@ public boolean isOffer() */ public boolean isRequest() { - return getOffererIfAny() == -1; + return !this.isTau() && getOffererIfAny() == -1; + } + + + /** + * Returns true if the action is a tau + * @return true if the action is a tau + */ + public boolean isTau() + { + return getTauMoverIfAny() != -1; } /** @@ -164,7 +206,13 @@ else if (this.isRequest()) */ @Override public Action getAction() { - if (this.isRequest()) + if (this.isTau()) + return this.getContent() + .stream() + .filter(TauAction.class::isInstance) + .findAny() + .orElseThrow(RuntimeException::new); + else if (this.isRequest()) return this.getContent() .stream() .filter(RequestAction.class::isInstance) @@ -188,7 +236,7 @@ public Action getAction() { public Action getCoAction() { Action action = this.getContent().stream() - .filter(s->!(s instanceof IdleAction)) + .filter(s->!(s instanceof IdleAction) && !(s instanceof TauAction)) .findAny().orElseThrow(IllegalArgumentException::new); if (this.isRequest()) { diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/label/action/TauAction.java b/src/main/java/io/github/contractautomata/catlib/automaton/label/action/TauAction.java new file mode 100644 index 00000000..f2b60ef9 --- /dev/null +++ b/src/main/java/io/github/contractautomata/catlib/automaton/label/action/TauAction.java @@ -0,0 +1,66 @@ +package io.github.contractautomata.catlib.automaton.label.action; + +import java.util.Objects; + +/** + * Class implementing a request action. + * + * @author Davide Basile + */ +public class TauAction extends Action { + + /** + * Constant symbol denoting a tau move + */ + public static final String TAU="tau_"; + + /** + * Constructor for a tau action + * @param label the label of this action + */ + public TauAction(String label) { + super(label); + } + + + /** + * Print a String representing this object + * @return a String representing this object + */ + @Override + public String toString(){ + return TAU+this.getLabel(); + } + + + /** + * A tau action matches no action. + * @param arg the other action to match + * @return true if this actions matches arg + */ + @Override + public boolean match(Action arg) { + return false; + } + + + /** + * Overrides the method of the object class + * @return the hashcode of this object + */ + @Override + public int hashCode() { + return Objects.hash(TAU+this.getLabel()); + } + + + /** + * Overrides the method of the object class + * @param o the other object to compare to + * @return true if the two objects are equal + */ + @Override + public boolean equals(Object o) { + return super.equals(o); + } +} diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/state/AbstractState.java b/src/main/java/io/github/contractautomata/catlib/automaton/state/AbstractState.java index 1122a293..bfdfaa9f 100644 --- a/src/main/java/io/github/contractautomata/catlib/automaton/state/AbstractState.java +++ b/src/main/java/io/github/contractautomata/catlib/automaton/state/AbstractState.java @@ -18,6 +18,7 @@ public abstract class AbstractState implements Ranked { */ private final T label; + /** * Constructs an abstract state from its label (content). * Label must be non-null diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/state/BasicState.java b/src/main/java/io/github/contractautomata/catlib/automaton/state/BasicState.java index 62869729..df4d615b 100644 --- a/src/main/java/io/github/contractautomata/catlib/automaton/state/BasicState.java +++ b/src/main/java/io/github/contractautomata/catlib/automaton/state/BasicState.java @@ -22,6 +22,8 @@ public class BasicState extends AbstractState{ */ private final boolean fin; + private boolean committed; + /** * Constructor for a BasicState. * Label must not be a list of elements, and elements @@ -38,6 +40,18 @@ public BasicState(T label, Boolean init, Boolean fin) { throw new UnsupportedOperationException(); this.init=init; this.fin=fin; + this.committed=false; + } + + public BasicState(T label, Boolean init, Boolean fin, boolean committed) { + super(label); + if (label instanceof List && ((List)label).get(0) instanceof AbstractState) + throw new UnsupportedOperationException(); + if (fin && committed) + throw new IllegalArgumentException(" A basic state cannot be both final and committed"); + this.init=init; + this.fin=fin; + this.committed=committed; } /** @@ -68,6 +82,11 @@ public boolean isInitial() { return init; } + public boolean isCommitted() {return committed;} + + + public void setCommitted() {committed=true;} + /** * Print a String representing this object * @return a String representing this object diff --git a/src/main/java/io/github/contractautomata/catlib/automaton/transition/ModalTransition.java b/src/main/java/io/github/contractautomata/catlib/automaton/transition/ModalTransition.java index f75b0d39..31848878 100644 --- a/src/main/java/io/github/contractautomata/catlib/automaton/transition/ModalTransition.java +++ b/src/main/java/io/github/contractautomata/catlib/automaton/transition/ModalTransition.java @@ -6,6 +6,7 @@ import io.github.contractautomata.catlib.automaton.label.CALabel; import io.github.contractautomata.catlib.automaton.label.Label; import io.github.contractautomata.catlib.automaton.label.action.Action; +import io.github.contractautomata.catlib.automaton.label.action.TauAction; import io.github.contractautomata.catlib.automaton.state.State; import io.github.contractautomata.catlib.operations.interfaces.TetraPredicate; import io.github.contractautomata.catlib.operations.interfaces.TriPredicate; @@ -83,8 +84,12 @@ public ModalTransition(S source, L label, S target, Modality type) super(source,label,target); if (type==null) throw new IllegalArgumentException(); - else - this.mod=type; + if (label.getContent() + .stream() + .anyMatch(TauAction.class::isInstance) + && type!=Modality.URGENT) + System.out.println("WARNING: a tau move is not urgent"); + this.mod=type; } /** diff --git a/src/main/java/io/github/contractautomata/catlib/converters/AutConverter.java b/src/main/java/io/github/contractautomata/catlib/converters/AutConverter.java index a5b1f29b..2bee619e 100644 --- a/src/main/java/io/github/contractautomata/catlib/converters/AutConverter.java +++ b/src/main/java/io/github/contractautomata/catlib/converters/AutConverter.java @@ -64,6 +64,8 @@ default Action parseAction(String action) { return new OfferAction(action.substring(1)); if (isAction.test(action, RequestAction.REQUEST)) return new RequestAction(action.substring(1)); + if (isAction.test(action, TauAction.TAU)) + return new TauAction(action.substring(4)); String[] f = action.split(Address.ACTION_SEPARATOR); String[] p = f[0].split(Address.ID_SEPARATOR); diff --git a/src/main/java/io/github/contractautomata/catlib/converters/AutDataConverter.java b/src/main/java/io/github/contractautomata/catlib/converters/AutDataConverter.java index 673967bf..3a251c79 100644 --- a/src/main/java/io/github/contractautomata/catlib/converters/AutDataConverter.java +++ b/src/main/java/io/github/contractautomata/catlib/converters/AutDataConverter.java @@ -73,6 +73,7 @@ public Automaton,ModalTransition(); Set> states = new HashSet<>(); Map>> mapBasicStates = new HashMap<>(); @@ -97,17 +98,22 @@ public Automaton,ModalTransitionArrays.stream(sar.split("[,|\\[]")) - .filter(s->!s.contains("Final states")) + .filter(s->!s.contains(commOrFin)) .map(String::trim) .filter(s->!s.isEmpty()) .toArray(String[]::new)) .toArray(String[][]::new); - if (fin.length!=rank) - throw new IllegalArgumentException("Final states with different rank"); - return fin; + if (states.length!=rank) + throw new IllegalArgumentException(commOrFin+" with different rank"); + return states; } private ModalTransition.Modality readModality(String strLine) { @@ -154,7 +160,7 @@ else if (ModalTransition.LAZY.equals(stype)) throw new IllegalArgumentException("Invalid modality"); } - private ModalTransition,L> loadTransition(String str, int rank, ModalTransition.Modality type, Set> states,Map>> mapBasicStates,String[] initial, String[][] fin) throws IOException + private ModalTransition,L> loadTransition(String str, int rank, ModalTransition.Modality type, Set> states,Map>> mapBasicStates,String[] initial, String[][] fin, String[][] comm) throws IOException { String regex = "\\(\\["+"(.+)"+"\\],\\["+"(.+)"+"\\],\\["+"(.+)"+"\\]\\)"; Pattern pattern = Pattern.compile(regex); @@ -172,8 +178,8 @@ private ModalTransition,L> loadTransition(String str tr[2].length!=rank) throw new IOException("Ill-formed transitions, different ranks"); - State source = createOrLoadState(states,mapBasicStates,tr[0],initial, fin);//source - State target = createOrLoadState(states,mapBasicStates,tr[2],initial, fin);//target + State source = createOrLoadState(states,mapBasicStates,tr[0],initial, fin, comm);//source + State target = createOrLoadState(states,mapBasicStates,tr[2],initial, fin, comm);//target return new ModalTransition<>(source,createLabel(tr),target,type); } @@ -188,7 +194,7 @@ private L createLabel(String[][] tr) { } - private State createOrLoadState(Set> states,Map>> mapBasicStates, String[] state,String[] initial, String[][] fin) { + private State createOrLoadState(Set> states,Map>> mapBasicStates, String[] state,String[] initial, String[][] fin, String[][] comm) { return states.stream() .filter(cs->IntStream.range(0, cs.getState().size()) @@ -203,7 +209,9 @@ private State createOrLoadState(Set> states,Map bs=new BasicState<>(state[i]+"", state[i].equals(initial[i]), - Arrays.stream(fin[i]).anyMatch(id->id.equals(state[i]))); + Arrays.stream(fin[i]).anyMatch(id->id.equals(state[i])), + iid.equals(state[i]))); if (l==null) mapBasicStates.put(i, new HashSet<>(List.of(bs))); else diff --git a/src/main/java/io/github/contractautomata/catlib/operations/CompositionFunction.java b/src/main/java/io/github/contractautomata/catlib/operations/CompositionFunction.java index 228f70f1..1834261a 100644 --- a/src/main/java/io/github/contractautomata/catlib/operations/CompositionFunction.java +++ b/src/main/java/io/github/contractautomata/catlib/operations/CompositionFunction.java @@ -75,6 +75,8 @@ public class CompositionFunction,L extends Label, private final Queue dontvisit; private final Predicate pruningPred; + private boolean ignoreModality; + //each transition of each MSCA in aut is associated with the corresponding index in aut final class TIndex {//more readable than Entry final T tra; @@ -129,6 +131,7 @@ public CompositionFunction(List aut, this.createTransition=createTransition; this.createAutomaton=createAutomaton; this.pruningPred=pruningPred; + this.ignoreModality=false; } /** @@ -171,41 +174,47 @@ else if (visited.add(sourceEntry.getKey())) //if the state has not been visited // .filter(e -> e.tra.getRank() != aut.get(e.ind).rank) // .count()==0); - Set>> trmap = computeComposedForwardStar(trans2index,source,sourcestate); - - //if source state is bad then don't visit target states - boolean badsourcestate = pruningPred!=null && trmap.parallelStream() - .anyMatch(x->pruningPred.test(x.getKey())&&x.getKey().isUrgent()); + //if source state is bad (more than one committed state) then don't visit target states + boolean badsourcestatecommitted = sourcestate.getState().stream().filter(BasicState::isCommitted).count()>1; - if (badsourcestate && sourcestate.equals(initialState)) + if (badsourcestatecommitted && sourcestate.equals(initialState)) return null; - else if (!badsourcestate) {//adding transitions, updating states - Set trans= trmap.parallelStream() - .filter(x -> pruningPred == null || x.getKey().isNecessary() || pruningPred.negate().test(x.getKey())) - .map(Entry::getKey).collect(toSet()); - tr.addAll(trans); - - if (pruningPred!=null)//avoid visiting targets of semicontrollable bad transitions - dontvisit.addAll(trans.parallelStream() - .filter(x->x.isLazy() && pruningPred.test(x)) - .map(T::getTarget) - .collect(toList())); - - toVisit.addAll(trmap.parallelStream() - .filter(x -> pruningPred == null || x.getKey().isNecessary() || pruningPred.negate().test(x.getKey())) - .map(Entry::getValue).collect(toSet()) - .parallelStream() - .map(s->new AbstractMap.SimpleEntry<>(s,sourceEntry.getValue()+1)) - .collect(toSet())); + else if (!badsourcestatecommitted) { + Set>> trmap = computeComposedForwardStar(trans2index, source, sourcestate); + + //if source state is bad (outgoing urgent transition violating pruning pred) then don't visit target states + boolean badsourcestateurgent = (pruningPred != null && !ignoreModality + && trmap.parallelStream().anyMatch(x -> pruningPred.test(x.getKey()) && x.getKey().isUrgent())); + + if (badsourcestateurgent && sourcestate.equals(initialState)) + return null; + else if (!badsourcestateurgent) {//adding transitions, updating states + Set trans = trmap.parallelStream() + .filter(x -> pruningPred == null ||(!ignoreModality && x.getKey().isNecessary()) || pruningPred.negate().test(x.getKey())) + .map(Entry::getKey).collect(toSet()); + tr.addAll(trans); + + if (pruningPred != null)//avoid visiting targets of semicontrollable bad transitions + dontvisit.addAll(trans.parallelStream() + .filter(x -> !ignoreModality && x.isLazy() && pruningPred.test(x)) + .map(T::getTarget) + .collect(toList())); + + toVisit.addAll(trmap.parallelStream() + .filter(x -> pruningPred == null || (!ignoreModality && x.getKey().isNecessary()) || pruningPred.negate().test(x.getKey())) + .map(Entry::getValue).collect(toSet()) + .parallelStream() + .map(s -> new AbstractMap.SimpleEntry<>(s, sourceEntry.getValue() + 1)) + .collect(toSet())); + } } } - } while (!toVisit.isEmpty()); //if (pruningPred==null) assert(new CompositionSpecCheck().test(aut, new MSCA(tr))); post-condition //in case of pruning if no final states are reachable return null - if (pruningPred!=null&& tr.parallelStream() + if (pruningPred!=null && tr.parallelStream() .flatMap(t->Stream.of(t.getSource(),t.getTarget())) .distinct().noneMatch(State::isFinalState)) return null; @@ -213,20 +222,25 @@ else if (!badsourcestate) {//adding transitions, updating states return this.createAutomaton.apply(tr); } - private Set>> computeComposedForwardStar(List trans2index,List source, S sourcestate){ + private Set>> computeComposedForwardStar(List trans2index,List source, S sourceState){ + int committed = IntStream.range(0,sourceState.getRank()) + .filter(i->sourceState.getState().get(i).isCommitted()) + .findFirst().orElse(-1); + List emptyList = new ArrayList<>(); //firstly match transitions are generated Map>>> matchTransitions= trans2index.parallelStream() .flatMap(e -> trans2index.parallelStream() + .filter(ee->(committed==-1)||(e.ind==committed)||(ee.ind==committed)) .filter(ee->(e.ind{ List targetlist = new ArrayList<>(source); targetlist.set(e.ind, e.tra.getTarget()); targetlist.set(ee.ind, ee.tra.getTarget()); - T tradd=createTransition.apply(sourcestate, + T tradd=createTransition.apply(sourceState, this.createLabel(e, ee), operandstat2compstat.computeIfAbsent(targetlist, s->createState.apply(flattenState(s))), e.tra.isNecessary()? @@ -244,12 +258,13 @@ private Set>> computeComposedForwardStar(List tran //collecting match transitions and adding unmatched transitions Set>> trmap = trans2index.parallelStream() + .filter(e->(committed==-1)||(e.ind==committed)) .filter(e -> !matchTransitions.containsKey(e.tra)) .map(e -> { List targetlist = new ArrayList<>(source); targetlist.set(e.ind, e.tra.getTarget()); return new SimpleEntry<> - (createTransition.apply(sourcestate, + (createTransition.apply(sourceState, this.shiftLabel(e.tra.getLabel(), rank, IntStream.range(0, e.ind) .map(i -> aut.get(i).getRank()) @@ -313,4 +328,10 @@ private L shiftLabel(L lab, Integer rank, Integer shift){ return createLabel.apply(l); } + + public void setIgnoreModality(){ + this.ignoreModality=true; + } + + } diff --git a/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingFunction.java b/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingFunction.java index fdf35f23..287ae173 100644 --- a/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingFunction.java +++ b/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingFunction.java @@ -2,6 +2,7 @@ import io.github.contractautomata.catlib.automaton.Automaton; import io.github.contractautomata.catlib.automaton.label.Label; +import io.github.contractautomata.catlib.automaton.label.action.TauAction; import io.github.contractautomata.catlib.automaton.state.BasicState; import io.github.contractautomata.catlib.automaton.state.State; import io.github.contractautomata.catlib.automaton.label.action.Action; @@ -32,11 +33,14 @@ * @author Davide Basile * */ -public class ModelCheckingFunction,L extends Label, - T extends ModalTransition,A extends Automaton> - extends CompositionFunction +public class ModelCheckingFunction, + L extends Label, + T extends ModalTransition, + A extends Automaton> extends CompositionFunction { + /** * The constructor of a model checking function.
* The match function of CompositionFunction is instantiated to match two labels with @@ -58,19 +62,26 @@ public ModelCheckingFunction(A aut, A prop, Function,L> createLabel, Function,A> createAutomaton) { super(Arrays.asList(aut, prop), - (l1,l2)-> l1.getAction() + (l1,l2)-> l1.getContent().stream() + .noneMatch(TauAction.class::isInstance)//do not match taus + && l1.getAction() .getLabel() .equals(l2.getContent().get(0).getLabel()), createState, createTransition, createLabel,createAutomaton, t->{ List listAct = t.getLabel().getContent(); - return ((listAct.get(t.getRank()-1) instanceof IdleAction)|| + return IntStream.range(0, t.getRank()-1) + .mapToObj(listAct::get) + .noneMatch(TauAction.class::isInstance) && //tau moves of aut are allowed + ((listAct.get(t.getRank()-1) instanceof IdleAction)|| IntStream.range(0, t.getRank()-1) .mapToObj(listAct::get) - .allMatch(IdleAction.class::isInstance));}); + .allMatch(IdleAction.class::isInstance));}); //pruning pred: aut and prop cannot be interleaved, if (prop.getRank()!=1) throw new IllegalArgumentException(); } + + } \ No newline at end of file diff --git a/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingSynthesisOperator.java b/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingSynthesisOperator.java index 7e0fd44b..1c7b7d32 100644 --- a/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingSynthesisOperator.java +++ b/src/main/java/io/github/contractautomata/catlib/operations/ModelCheckingSynthesisOperator.java @@ -42,6 +42,7 @@ public class ModelCheckingSynthesisOperator> extends SynthesisOperator { + private final A2 prop; private final UnaryOperator changeLabel; private final Function,L> createLabel; @@ -50,6 +51,9 @@ public class ModelCheckingSynthesisOperator,L2> createLabelProp; private final TetraFunction createTransitionProp; private final Function,A2> createAutomatonProp; + private boolean ignoreModality; + + /** * Constructor for a model checking synthesis operator, it requires also the constructors for the used generic types. @@ -90,6 +94,7 @@ public ModelCheckingSynthesisOperator( this.createLabelProp=createLabelProp; this.createTransitionProp=createTransitionProp; this.createAutomatonProp=createAutomatonProp; + this.ignoreModality=false; } /** @@ -163,7 +168,6 @@ public A apply(A arg1) { //model checking is performed on the type of the property (the resulting labels //could not be calabels), whilst the synthesis is performed using the type of the automaton //(generally requirements are expressed using calabels), thus conversions must be performed - A2 convertAut = createAutomatonProp.apply( //converting A to A2 arg1.getTransition() .parallelStream() @@ -173,45 +177,81 @@ public A apply(A arg1) { t.getModality())) .collect(Collectors.toSet())); +// //model checking may be performed on the automaton where modalities are ignored (i.e., all +// //necessary transitions are turned to optional for the model checking phase) +// HideModality hm = new HideModality<>(convertAut, createTransitionProp, createAutomatonProp); +// +// if (ignoreModality) { +// convertAut = hm.getAutAllPermitted(); +// } + ModelCheckingFunction mcf = new ModelCheckingFunction<>(convertAut,prop, createState, createTransitionProp, createLabelProp, createAutomatonProp); + if (ignoreModality) mcf.setIgnoreModality(); + A2 comp = mcf.apply(Integer.MAX_VALUE); if (comp==null) return null; - //the following steps are necessary to reuse the synthesis, reverting A2 to A, - //silencing the prop action and treat lazy transitions satisfying the pruningPredicate: - //they must be detectable as "bad" also after reverting to A, - //lazy transitions are quantified existentially on the states: the states must not be modified - A deletingPropAction = this.getCreateAut().apply(comp.getTransition() - .parallelStream().map(t->{ - List li = new ArrayList<>(t.getLabel().getContent()); - li.set(t.getRank()-1, new IdleAction()); //silencing the prop moves - L lab = createLabel.apply(li); - if (mcf.getPruningPred().test(t) - && t.isLazy() - && this.getReq().test(lab)) //the transition was lazy and bad (satisfying pruning pred), - // but after removing the prop move it satisfies getReq: it must be changed. - lab=changeLabel.apply(lab); //change either to request or offer - return createTransition.apply( - t.getSource(), - lab, - t.getTarget(), - t.getModality());}) - .collect(Collectors.toSet())); + A deletingPropAction; + +// //in case necessary modalities were ignored, they will be restored on the model checked automaton +// if (ignoreModality) { +// //to restore the modalities, firstly we need to remove the principal corresponding to the property +// RemovePrincipalOperator +// rp = new RemovePrincipalOperator<>(createState, createTransitionProp, createAutomatonProp, createLabelProp); +// comp = rp.apply(comp, comp.getRank()-1); +// +// comp = hm.getAutWithMod(comp); +// +// /* it is not clear whether I have to use changeLabel also in this case, +// as in the case where modalities have not been ignored. +// Furthermore, for portability, the principal of the property is only removed +// inside this branch.*/ +// //reverting A2 to A +// deletingPropAction = this.getCreateAut().apply(comp.getTransition().parallelStream() +// .map(t-> +// createTransition.apply(t.getSource(),createLabel.apply(t.getLabel().getContent()),t.getTarget(),t.getModality()) +// ).collect(Collectors.toSet())); +// } +// else + { + //the following steps are necessary to reuse the synthesis, reverting A2 to A, + //silencing the prop action and treat lazy transitions satisfying the pruningPredicate: + //they must be detectable as "bad" also after reverting to A. + //Transitions not satisfying the pruning predicate of mcf are basically moves of the automaton + //not allowed by the property. If they are lazy, the mcf does not prune them. + //To remind that they were violating the property, e.g., in case of an orchestration, it is + //transformed into a necessary not matched request. Note that this transformation is only + //necessary if the transition is not already detected as violating either agreement or strong agreement. + //lazy transitions are quantified existentially on the states: the states must not be modified + deletingPropAction = this.getCreateAut().apply(comp.getTransition() + .parallelStream().map(t -> { + List li = new ArrayList<>(t.getLabel().getContent()); + li.set(t.getRank() - 1, new IdleAction()); //silencing the prop moves + L lab = createLabel.apply(li); + if (mcf.getPruningPred().test(t) //the pruning pred of mcf does not allow interleavings of the automaton and the property + && t.isLazy() + && this.getReq().test(lab)) //the transition was lazy and bad (satisfying pruning pred), + // but after removing the prop move it satisfies getReq: it must be changed. + lab = changeLabel.apply(lab); //change either to request or offer + return createTransition.apply( + t.getSource(), + lab, + t.getTarget(), + t.getModality()); + }) + .collect(Collectors.toSet())); + } //computing the synthesis return super.apply(deletingPropAction); } } - public A2 getProp() { - return prop; - } - /** * Getter of the function changeLabel. * @@ -220,4 +260,9 @@ public A2 getProp() { public UnaryOperator getChangeLabel(){ return this.changeLabel; } + + + public void setIgnoreModality() { + this.ignoreModality = true; + } } \ No newline at end of file diff --git a/src/main/java/io/github/contractautomata/catlib/operations/NewOrchestrationSynthesisOperator.java b/src/main/java/io/github/contractautomata/catlib/operations/NewOrchestrationSynthesisOperator.java index 5ef4cce4..0701861a 100644 --- a/src/main/java/io/github/contractautomata/catlib/operations/NewOrchestrationSynthesisOperator.java +++ b/src/main/java/io/github/contractautomata/catlib/operations/NewOrchestrationSynthesisOperator.java @@ -2,58 +2,89 @@ import io.github.contractautomata.catlib.automaton.Automaton; import io.github.contractautomata.catlib.automaton.label.CALabel; -import io.github.contractautomata.catlib.automaton.label.action.Action; -import io.github.contractautomata.catlib.automaton.label.action.IdleAction; -import io.github.contractautomata.catlib.automaton.label.action.OfferAction; +import io.github.contractautomata.catlib.automaton.label.Label; +import io.github.contractautomata.catlib.automaton.label.action.*; import io.github.contractautomata.catlib.automaton.state.BasicState; import io.github.contractautomata.catlib.automaton.state.State; import io.github.contractautomata.catlib.automaton.transition.ModalTransition; import io.github.contractautomata.catlib.automaton.transition.Transition; +import io.github.contractautomata.catlib.converters.AutDataConverter; +import jdk.jfr.Percentage; +import java.io.IOException; import java.util.*; import java.util.function.Predicate; import java.util.stream.Collectors; import java.util.stream.IntStream; +import static io.github.contractautomata.catlib.automaton.transition.ModalTransition.Modality.PERMITTED; +import static io.github.contractautomata.catlib.automaton.transition.ModalTransition.Modality.URGENT; + /** * Class implementing the new orchestration synthesis operator.
* - * * @author Davide Basile * */ -public class NewOrchestrationSynthesisOperator +public class NewOrchestrationSynthesisOperator extends MpcSynthesisOperator { - private final Predicate req; - public NewOrchestrationSynthesisOperator(Predicate req){ - this.req=req; + super(req); + + } + + public NewOrchestrationSynthesisOperator(Predicate req, Automaton,ModalTransition,Label>> prop){ + super(req,prop); + } + + @Override + public Automaton,ModalTransition,CALabel>> apply(Automaton,ModalTransition,CALabel>> aut) + { + ProjectionFunction pf = new ProjectionFunction<>(); + return this.apply(IntStream.range(0, aut.getRank()) + .mapToObj(i->pf.apply(aut,i,t->t.getLabel().getRequester())) + .collect(Collectors.toList())); } /** * Applies the orchestration synthesis to aut. - * The automata must not contain necessary offers. * - * @param laut the list of automaton to compose to obtain the plant automaton, to which the mpc synthesis is applied - * @return the synthesised orchestration. */ public Automaton,ModalTransition,CALabel>> apply(List,ModalTransition,CALabel>>> laut) { if (laut.stream() .map(Automaton::getTransition) - .anyMatch(s->s.parallelStream() - .anyMatch(t-> !t.isPermitted()&&t.getLabel().isOffer() || t.getLabel().getAction().getLabel().startsWith("tau_")))) - throw new UnsupportedOperationException("Some automaton contains necessary offers that are not allowed in the orchestration synthesis or some action is labelled with tau_"); + .anyMatch(ts->ts.parallelStream() + .anyMatch(t-> (!t.isPermitted()&&t.getLabel().isOffer()) || t.getLabel().isTau()))) + throw new IllegalArgumentException("Some automaton contains necessary offers that are not allowed in the orchestration synthesis or some action is tau"); + + if (laut.stream() + .anyMatch(a->a.getRank()>1)) + throw new IllegalArgumentException("Only principals are allowed"); + + //compose encoded principals + Automaton, ModalTransition, CALabel>> comp = + new MSCACompositionFunction<>(encodePrincipals(laut), t->this.getReq().negate().test(t.getLabel())).apply(Integer.MAX_VALUE); - if (laut.stream().anyMatch(a->a.getRank()>1)) - throw new UnsupportedOperationException("All automata must be principal"); + //apply mpc synthesis to the encoded automata + Automaton, ModalTransition, CALabel>> mpc = super.apply(comp); - List, ModalTransition, CALabel>>> backup = laut; + if (Objects.isNull(mpc)) + return null; - //encode the principal automata - laut = laut.stream() + return mpc;//decode(mpc,laut); + } + + + /** + * each lazy transition is unfolded into an urgent tau move followed by an optional transition with the same original label. + * It is necessary to introduce a new state, with a new state label. Therefore, the type of the label of the state + * is instantiated to String. + */ + private List,ModalTransition,CALabel>>> encodePrincipals(List,ModalTransition,CALabel>>> laut){ + return laut.stream() .map(aut-> { //each lazy transition is unfolded into two linked transitions, one uncontrollable and one controllable @@ -69,21 +100,16 @@ public Automaton,ModalTransition> intermediate = new ArrayList<>(t.getSource().getState()); - if (t.getLabel().isOffer() || t.getLabel().isMatch()) { - label.set(t.getLabel().getOfferer(), new OfferAction("tau_" + t.getLabel().getAction().getLabel())); - String stateLabel = t.getSource().getState().get(t.getLabel().getOfferer()).getState() + "_" + t.getLabel().getAction().getLabel() + "_" + t.getTarget().getState().get(t.getLabel().getOfferer()).getState(); - intermediate.set(t.getLabel().getOfferer(), new BasicState<>(stateLabel, false, false));//the new basic state has the same label of the source - } - + //the checks at the beginning of the method ensures that only necessary requests are lazy, and principals cannot have matches if (t.getLabel().isRequest()) { - label.set(t.getLabel().getRequester(), new OfferAction("tau_" + t.getLabel().getAction().getLabel()));//the label cannot be a request + label.set(t.getLabel().getRequester(), new TauAction(t.getLabel().getAction().getLabel()));//the label cannot be a request String stateLabel = t.getSource().getState().get(t.getLabel().getRequester()).getState() + "_" + t.getLabel().getAction().getLabel() + "_" + t.getTarget().getState().get(t.getLabel().getRequester()).getState(); intermediate.set(t.getLabel().getRequester(), new BasicState<>(stateLabel, false, false)); } State intermediateState = new State<>(intermediate); - ModalTransition, CALabel> t1 = new ModalTransition<>(t.getSource(), new CALabel(label), intermediateState, ModalTransition.Modality.URGENT); - ModalTransition, CALabel> t2 = new ModalTransition<>(intermediateState, t.getLabel(), t.getTarget(), ModalTransition.Modality.PERMITTED); + ModalTransition, CALabel> t1 = new ModalTransition<>(t.getSource(), new CALabel(label), intermediateState, URGENT); + ModalTransition, CALabel> t2 = new ModalTransition<>(intermediateState, t.getLabel(), t.getTarget(), PERMITTED); return List.of(t1, t2); } })); @@ -93,77 +119,185 @@ public Automaton,ModalTransition map.get(t).stream()) .collect(Collectors.toSet())); }).collect(Collectors.toList()); + } +// /** +// * remove the tau moves. However, it introduces non-determinism +// */ +// private Automaton,ModalTransition,CALabel>> decode(Automaton,ModalTransition,CALabel>> mpc, +// List,ModalTransition,CALabel>>> laut){ +// +// //decode the orchestration +// Set, CALabel>> str = mpc.getTransition(); +// +// //for each state, perform a visit traversing only tau moves, and add each non-tau outgoing +// //transition from each visited state to the starting state of the visit +// str.addAll(mpc.getStates().parallelStream() +// .flatMap(startstate->{ +// Map,Boolean> map = mpc.getStates().stream() +// .collect(Collectors.toMap(x -> x, x -> false)); +// map.put(startstate, true); +// Queue> toVisit = new LinkedList<>(List.of(startstate)); +// Set, CALabel>> newTrans = new HashSet<>(); +// while(!toVisit.isEmpty()) { +// State currentstate = toVisit.remove(); +// newTrans.addAll(mpc.getForwardStar(currentstate) +// .stream() +// .filter(t->!t.getLabel().isTau()) +// .map(t->new ModalTransition<>(startstate,t.getLabel(),t.getTarget(), t.getModality())) +// .collect(Collectors.toSet())); +// Map, Boolean> toAdd = +// mpc.getForwardStar(currentstate).stream() +// .filter(t -> t.getLabel().isTau() && +// Boolean.FALSE.equals(map.get(t.getTarget()))) +// .map(Transition::getTarget) +// .distinct() +// .collect(Collectors.toMap(x -> x, x -> true)); +// map.putAll(toAdd); +// toVisit.addAll(toAdd.keySet()); +// } +// return newTrans.stream();}) +// .collect(Collectors.toSet())); +// +// //removing the tau moves +// str = str.parallelStream() +// .filter(t -> !t.getLabel().isTau()) +// .collect(Collectors.toSet()); +// +// //restore the lazy modality for the interested transitions +// str = str.parallelStream() +// .map(t->{ +// if (t.getLabel().isOffer()) +// return t; +// int requester = t.getLabel().getRequester(); +// String state = t.getSource().getState().get(requester).getState().split("_")[0]; +// String action = t.getLabel().getAction().getLabel(); +// if (laut.get(requester).getTransition().stream() +// .anyMatch(pt-> +// pt.getSource().getState().get(0).getState().equals(state) && +// pt.getLabel().getAction().getLabel().equals(action) && +// pt.getModality().equals(ModalTransition.Modality.LAZY))) +// return new ModalTransition<>(t.getSource(),t.getLabel(),t.getTarget(), ModalTransition.Modality.LAZY); +// else +// return t; +// +// }).collect(Collectors.toSet()); +// +// //remove dangling states and transitions (the synthesis is reused) +// return new OrchestrationSynthesisOperator(this.getReq()).apply(new Automaton<>(str)); +// } - //compose and apply mpc synthesis to the encoded automaton - - Automaton, ModalTransition, CALabel>> comp = - new MSCACompositionFunction<>(laut, t->t.getLabel().isRequest()).apply(Integer.MAX_VALUE); - - Automaton, ModalTransition, CALabel>> mpc = - new MpcSynthesisOperator(this.req).apply(comp); +} +//END OF CLASS - if (Objects.isNull(mpc)) - return null; - //decode the orchestration - Set, CALabel>> str = mpc.getTransition(); - - //for each state, perform a visit traversing only tau moves, and add each non-tau outgoing - //transition from each visited state to the starting state of the visit - str.addAll(mpc.getStates().parallelStream() - .flatMap(startstate->{ - Map,Boolean> map = mpc.getStates().stream() - .collect(Collectors.toMap(x -> x, x -> false)); - map.put(startstate, true); - Queue> toVisit = new LinkedList<>(List.of(startstate)); - Set, CALabel>> newTrans = new HashSet<>(); - while(!toVisit.isEmpty()) { - State currentstate = toVisit.remove(); - newTrans.addAll(mpc.getForwardStar(currentstate) - .stream() - .filter(t->!t.isUrgent()) - .map(t->new ModalTransition<>(startstate,t.getLabel(),t.getTarget(), t.getModality())) - .collect(Collectors.toSet())); - Map, Boolean> toAdd = - mpc.getForwardStar(currentstate).stream() - .filter(t -> t.isUrgent() && - Boolean.FALSE.equals(map.get(t.getTarget()))) - .map(Transition::getTarget) - .distinct() - .collect(Collectors.toMap(x -> x, x -> true)); - map.putAll(toAdd); - toVisit.addAll(toAdd.keySet()); - } - return newTrans.stream();}) - .collect(Collectors.toSet())); - - //removing the tau moves - str = str.parallelStream() - .filter(t -> !t.getLabel().getAction().getLabel().startsWith("tau_")) - .collect(Collectors.toSet()); - - //restore the lazy modality for the interested transitions - str = str.parallelStream() - .map(t->{ - if (t.getLabel().isOffer()) - return t; - int requester = t.getLabel().getRequester(); - String state = t.getSource().getState().get(requester).getState().split("_")[0]; - String action = t.getLabel().getAction().getLabel(); - if (backup.get(requester).getTransition().stream() - .anyMatch(pt-> - pt.getSource().getState().get(0).getState().equals(state) && - pt.getLabel().getAction().getLabel().equals(action) && - pt.getModality().equals(ModalTransition.Modality.LAZY))) - return new ModalTransition<>(t.getSource(),t.getLabel(),t.getTarget(), ModalTransition.Modality.LAZY); - else - return t; - - }).collect(Collectors.toSet()); - - //remove dangling states and transitions (the synthesis is reused) - return new OrchestrationSynthesisOperator(this.req).apply(new Automaton<>(str)); - - } -} \ No newline at end of file +// +// private Automaton,ModalTransition,CALabel>> encode(Automaton,ModalTransition,CALabel>> aut) { +// Set, CALabel>> ts = aut.getTransition(); +// +// Set, CALabel>> removed = new HashSet<>(); +// ModalTransition, CALabel> t = ts.stream() +// .filter(ModalTransition::isLazy) +// .findFirst().orElse(null); +// +// int ind=0; +// while(t!=null) +// { +//// try { +//// new AutDataConverter<>(CALabel::new).exportMSCA("test_"+ind, new Automaton<>(ts)); +//// } catch (IOException e) { +//// throw new RuntimeException(e); +//// } +// removed.add(t); +// State source = t.getSource(); +// final int requester = t.getLabel().getRequester(); +// +// List label = IntStream.range(0, t.getLabel().getRank()) +// .mapToObj(i -> new IdleAction()) +// .collect(Collectors.toList()); +// +// List> intermediate = new ArrayList<>(source.getState()); +// +// //the checks at the beginning of the method ensures that only necessary requests and matches are lazy +// //if it is lazy there is always a requester +// label.set(requester, new OfferAction("tau_" + t.getLabel().getAction().getLabel()));//the label cannot be a request +// String stateLabelReq = t.getSource().getState().get(requester).getState() + "_" + t.getLabel().getAction().getLabel() + "_" + t.getTarget().getState().get(requester).getState(); +// intermediate.set(requester, new BasicState<>(stateLabelReq, false, false)); +// +// //in case of match set also the offerer +//// if (t.getLabel().isMatch()){ +//// label.set(t.getLabel().getOfferer(), new RequestAction("tau_" + t.getLabel().getAction().getLabel()));//the label cannot be a request +//// String stateLabelOff = t.getSource().getState().get(t.getLabel().getOfferer()).getState() + "_" + t.getLabel().getAction().getLabel() + "_" + t.getTarget().getState().get(t.getLabel().getOfferer()).getState(); +//// intermediate.set(t.getLabel().getOfferer(), new BasicState<>(stateLabelOff, false, false)); +//// } +// +// State intermediateState = new State<>(intermediate); +// ts.remove(t); +// ts.addAll(ts.parallelStream() +// .filter(x->x.getSource().equals(source)) +// .filter(x -> !removed.contains(x) && (x.getLabel().getContent().get(requester) instanceof IdleAction)) +// .map(tr -> new ModalTransition<>(intermediateState, tr.getLabel(), tr.getTarget(), tr.getModality())) +// .collect(Collectors.toSet())); +// ts.add(new ModalTransition<>(source, new CALabel(label), intermediateState, URGENT)); +// ts.add(new ModalTransition<>(intermediateState, t.getLabel(), t.getTarget(), PERMITTED)); +// t = ts.stream() +// .filter(ModalTransition::isLazy) +// .findFirst().orElse(null); +// +// ind++; +// } +// return new Automaton<>(ts); +// } +// private Automaton,ModalTransition, Label>> encodeProp(Automaton,ModalTransition, Label>> prop) +// { +// if (Objects.isNull(prop)) +// return null; +// Set, Label>> ts = prop.getTransition(); +// +// ModalTransition, Label> t = ts.stream() +// .filter(ModalTransition::isLazy) +// .findFirst().orElse(null); +// Set, Label>> removed = new HashSet<>(); +// while(t!=null) +// { +// removed.add(t); +// BasicState bs = new BasicState<>(t.getSource().getState().get(0).getState() + "_tau" + t.getLabel().getAction().getLabel(),false, false); +// State source = t.getSource(); +// State intermediate = new State<>(List.of(bs)); +// Label tau = new Label<>(List.of(new Action("tau_" + t.getLabel().getAction().getLabel()))); +// ts.remove(t); +// ts.addAll(ts.parallelStream() +// .filter(x->x.getSource().equals(source)) +// .filter(tr -> !removed.contains(tr)) +// .map(tr -> new ModalTransition<>(intermediate, tr.getLabel(), tr.getTarget(), tr.getModality())) +// .collect(Collectors.toSet())); +// ts.add(new ModalTransition<>(source, tau, intermediate, PERMITTED)); +// ts.add(new ModalTransition<>(intermediate, t.getLabel(), t.getTarget(), PERMITTED)); +// t = ts.stream() +// .filter(ModalTransition::isLazy) +// .findFirst().orElse(null); +// } +// return new Automaton<>(ts); +// } +// +/** + // * the property accepts also all tau moves of the automaton comp + // */ +// private Automaton,ModalTransition, Label>> addTaus(Automaton,ModalTransition, Label>> prop, +// Automaton, ModalTransition, CALabel>> comp){ +// if (Objects.isNull(prop)) +// return null; +// Set taus = comp.getTransition().parallelStream() +// .map(t->t.getLabel().getAction().getLabel()) +// .filter(s->s.startsWith("tau_")) +// .collect(Collectors.toSet()); +// +// Set, Label>> collect = prop.getStates().stream() +// .flatMap(s -> taus.stream() +// .map(act -> new ModalTransition<>(s, new Label<>(List.of(new Action(act))), s, PERMITTED))) +// .collect(Collectors.toSet()); +// +// collect.addAll(prop.getTransition()); +// +// return new Automaton<>(collect); +// } \ No newline at end of file diff --git a/src/main/java/io/github/contractautomata/catlib/operations/RemovePrincipalOperator.java b/src/main/java/io/github/contractautomata/catlib/operations/RemovePrincipalOperator.java new file mode 100644 index 00000000..c1004c45 --- /dev/null +++ b/src/main/java/io/github/contractautomata/catlib/operations/RemovePrincipalOperator.java @@ -0,0 +1,73 @@ +package io.github.contractautomata.catlib.operations; + +import io.github.contractautomata.catlib.automaton.Automaton; +import io.github.contractautomata.catlib.automaton.label.CALabel; +import io.github.contractautomata.catlib.automaton.label.Label; +import io.github.contractautomata.catlib.automaton.label.action.Action; +import io.github.contractautomata.catlib.automaton.label.action.IdleAction; +import io.github.contractautomata.catlib.automaton.state.BasicState; +import io.github.contractautomata.catlib.automaton.state.State; +import io.github.contractautomata.catlib.automaton.transition.ModalTransition; +import io.github.contractautomata.catlib.operations.interfaces.TetraFunction; + +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +public class RemovePrincipalOperator, + L extends Label, + T extends ModalTransition, + A extends Automaton> implements BiFunction { + + private final TetraFunction createTransition; + private final Function,A> createAutomaton; + private final Function>,S> createState; + private final Function,L> createLabel; + + public RemovePrincipalOperator( Function>,S> createState, + TetraFunction createTransition, + Function,A> createAutomaton, + Function,L> createLabel){ + this.createState=createState; + this.createTransition=createTransition; + this.createAutomaton=createAutomaton; + this.createLabel=createLabel; + + } + + @Override + public A apply(A aut, Integer i){ + if (i>=aut.getRank()) + throw new IllegalArgumentException("The index of the principal is greater than the rank of the automaton"); + + Function>, List>> remove_i = l -> { + l.remove((int) i); + return l; + }; + Map>, S> mapState = aut.getStates() + .parallelStream() + .map(s->remove_i.apply(s.getState())) + .distinct() + .collect(Collectors.toMap(s->s, createState)); + + Set setTr = aut.getTransition().parallelStream() + .filter(t-> IntStream.range(0,t.getRank()) + .filter(j->j!=i) + .anyMatch(j->!(t.getLabel().getContent().get(j) instanceof IdleAction))) + //filter out transitions where all principals, apart from i, are idle + .map(t->{ + List label = t.getLabel().getContent(); + label.remove((int) i); + return createTransition.apply(mapState.get(remove_i.apply(t.getSource().getState())),createLabel.apply(label), + mapState.get(remove_i.apply(t.getTarget().getState())),t.getModality()); + }).collect(Collectors.toSet()); + + return createAutomaton.apply(setTr); + } +} diff --git a/src/main/java/io/github/contractautomata/catlib/requirements/StrongAgreement.java b/src/main/java/io/github/contractautomata/catlib/requirements/StrongAgreement.java index 48857f8f..a73ed80a 100644 --- a/src/main/java/io/github/contractautomata/catlib/requirements/StrongAgreement.java +++ b/src/main/java/io/github/contractautomata/catlib/requirements/StrongAgreement.java @@ -14,13 +14,13 @@ public class StrongAgreement implements Predicate { /** - * Returns true if l is a match. + * Returns true if l is a match, ignore tau moves. * @param l the label to test. - * @return true if l is a match. + * @return true if l is a match, ignore tau moves. */ @Override public boolean test(CALabel l) { - return l.isMatch(); + return l.isMatch() || l.isTau(); } } diff --git a/src/main/java/io/github/contractautomata/catlib/toignore/DkBricsEncoder.java b/src/main/java/io/github/contractautomata/catlib/toignore/DkBricsEncoder.java new file mode 100644 index 00000000..43d6878e --- /dev/null +++ b/src/main/java/io/github/contractautomata/catlib/toignore/DkBricsEncoder.java @@ -0,0 +1,125 @@ +package io.github.contractautomata.catlib.toignore; + +/** + * THIS CLASS IS NOT WORKING. + * THE CODE IS LEFT IN CASE IT MAY BE NEEDED FOR OTHER ENCODERS. + * + * I have encountered the following issues with the library dk.brics.automaton.Automaton. + * It is hard to keep a connection between the states of the starting contract automaton, + * and the states of the automaton encoded into the dk.brics library. + * This is because at each operation of the dk.brics library, states are instantiated as + * new objects (the method equals for state is the one from Object class). + * Furthermore, there is no way of assigning additional information to a state, for example, + * a label, in such a way that a state can be identified by its label, even if the object + * is new. + * Indeed, the dk.brics library assigns an integer to each state, which however varies + * at every new operation (e.g., toString, toDot), so each number does not uniquely identify + * a state through various operations. + * Furthermore, although I can extend a State to include a label, each operation called + * to the automaton will produce a new automaton such that states have no label. + */ +public class DkBricsEncoder { +// +// private Map> dkstate2castate; +// private Map, dk.brics.automaton.State> castate2dkstate; +// +// private Map transition2modality; +// +// private Map label2char; +// +// private Map char2label; +// +// private dk.brics.automaton.Automaton dkAut; +// +// public DkBricsEncoder(io.github.contractautomata.catlib.automaton.Automaton, ModalTransition, CALabel>> aut) { +// dk.brics.automaton.Automaton a = new dk.brics.automaton.Automaton(); +// +// List labels = aut.getTransition().parallelStream() +// .map(io.github.contractautomata.catlib.automaton.transition.Transition::getLabel) +// .distinct() +// .collect(Collectors.toList()); +// +// if (labels.size()>127) //ASCII interval +// throw new RuntimeException("Cannot encode all the labels into chars"); +// +// label2char = IntStream.range(0,labels.size()) +// .boxed() +// .collect(Collectors.toMap(labels::get, i-> (char) i.intValue())); +// +// char2label = label2char.entrySet() +// .stream() +// .collect(Collectors.toMap(Map.Entry::getValue, Map.Entry::getKey)); +// +// dkstate2castate = aut.getStates().parallelStream() +// .collect(Collectors.toMap(s -> { +// dk.brics.automaton.State state = new dk.brics.automaton.State(); +// if (s.isInitial()) a.setInitialState(state); +// if (s.isFinalState()) state.setAccept(true); +// return state; +// }, s -> s)); +// +// castate2dkstate = dkstate2castate.entrySet() +// .stream() +// .collect(Collectors.toMap(Map.Entry::getValue, Map.Entry::getKey)); +// +// transition2modality = new HashMap<>(); +// +// dkstate2castate.keySet().forEach( +// state -> { +// aut.getForwardStar(dkstate2castate.get(state)).forEach( +// tr -> { +// dk.brics.automaton.State target = castate2dkstate.get(tr.getTarget()); +// Character label = label2char.get(tr.getLabel()); +// Transition t = new Transition(label, target); +// transition2modality.put(t,tr.getModality()); +// state.addTransition(t); +// }); +// } +// +// ); +// +//// a.toDot(); //this is used to set the state numbers, which is done inside the method... +//// dkstatestring2castate = dkstate2castate.entrySet() +//// .stream() +//// //.peek(e->System.out.println(e.getKey())) +//// .collect(Collectors.toMap(e->e.getKey().toString().split(":")[0], Map.Entry::getValue)); +// +// +// // System.out.println(transition2modality); +// this.dkAut=a; +// } +// +// public Automaton getDkAut(){ +// return dkAut; +// } +// +// +// public io.github.contractautomata.catlib.automaton.Automaton, ModalTransition, CALabel>> getCA(){ +// Map map = dkAut.getStates().stream() +// .collect(Collectors.toMap(x -> x, x -> false)); +// map.put(dkAut.getInitialState(), true); +// Queue toVisit = new LinkedList<>(List.of(dkAut.getInitialState())); +// Set, CALabel>> trans = new HashSet<>(); +// while(!toVisit.isEmpty()) { +// dk.brics.automaton.State currentstate = toVisit.remove(); +// //System.out.println(currentstate.toString().split(":")[0]); +// // System.out.println(dkstatestring2castate); +// trans.addAll(currentstate.getTransitions() +// .stream() +// // .peek(t-> { System.out.println(dkstatestring2castate.get(currentstate.toString().split(":")[0]) + " " + char2label.get(t.getMin()) + " " + dkstatestring2castate.get(t.getDest().toString().split(":")[0])); }) +// .map(t->{ +// return new ModalTransition<>(dkstate2castate.get(currentstate),char2label.get(t.getMin()),dkstate2castate.get(t.getDest()), transition2modality.get(t)); +// }) +// .collect(Collectors.toSet())); +// Map toAdd = +// currentstate.getTransitions() +// .stream() +// .map(Transition::getDest) +// .filter(dest ->Boolean.FALSE.equals(map.get(dest))) +// .distinct() +// .collect(Collectors.toMap(x -> x, x -> true)); +// map.putAll(toAdd); +// toVisit.addAll(toAdd.keySet()); +// } +// } +} diff --git a/src/main/java/io/github/contractautomata/catlib/toignore/HideNecessaryModality.java b/src/main/java/io/github/contractautomata/catlib/toignore/HideNecessaryModality.java new file mode 100644 index 00000000..1af41053 --- /dev/null +++ b/src/main/java/io/github/contractautomata/catlib/toignore/HideNecessaryModality.java @@ -0,0 +1,87 @@ +package io.github.contractautomata.catlib.toignore; + +import io.github.contractautomata.catlib.automaton.Automaton; +import io.github.contractautomata.catlib.automaton.label.Label; +import io.github.contractautomata.catlib.automaton.label.action.Action; +import io.github.contractautomata.catlib.automaton.state.State; +import io.github.contractautomata.catlib.automaton.transition.ModalTransition; +import io.github.contractautomata.catlib.automaton.transition.Transition; +import io.github.contractautomata.catlib.operations.interfaces.TetraFunction; + +import java.util.Map; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * this class is used to turn all transitions of an automaton to permitted, + * and revert them. + * The idea was to perform model checking on an automaton where also necessary + * transitions can be pruned. Therefore, first necessary transitions are hidden, + * model checking is applied, and the transitions are reverted to necessary + * on the automaton result of the model checking. + * + * This has been later changed so that the composition already can ignore modalities. + * + * @param + * @param + * @param + * @param + * @param + */ +public class HideNecessaryModality, + L extends Label, + T extends ModalTransition, + A extends Automaton> { + + private final Map, T> tr2modtr; + + private final Map> string2tr; + + private final TetraFunction createTransition; + private final Function,A> createAutomaton; + + + public HideNecessaryModality(A aut, + TetraFunction createTransition, + Function,A> createAutomaton){ + this.createTransition=createTransition; + this.createAutomaton=createAutomaton; + + tr2modtr = aut.getTransition().parallelStream() + .collect(Collectors.toMap(t->new Transition<>(t.getSource(),t.getLabel(),t.getTarget()), t->t)); + +// Map> modtr2tr = tr2modtr.entrySet() +// .stream() +// .collect(Collectors.toMap(Map.Entry::getValue, Map.Entry::getKey)); + + string2tr = tr2modtr.keySet().stream() + .collect(Collectors.toMap(Transition::toString, t->t)); + } + + public A getAutAllPermitted(){ + return createAutomaton.apply(tr2modtr.keySet() + .parallelStream() + .map(t->createTransition.apply(t.getSource(),t.getLabel(),t.getTarget(), ModalTransition.Modality.PERMITTED)) + .collect(Collectors.toSet())); + } + + public A getAutWithNecessary(A aut){ + return createAutomaton.apply(aut.getTransition().parallelStream() + .map(t->tr2modtr.get(string2tr.get(new Transition<>(t.getSource(),t.getLabel(),t.getTarget()).toString()))) + .collect(Collectors.toSet())); + } + + +// public Automaton> getEncoded(){ +// return new Automaton<>(tr2modtr.keySet()); +// } +// +// public A decode( Automaton> aut){ +// return createAutomaton.apply(aut.getTransition().parallelStream() +// .map(t->tr2modtr.get(string2tr.get(t.toString()))) +// .collect(Collectors.toSet())); +// } + +} \ No newline at end of file diff --git a/src/test/java/io/github/contractautomata/catlib/automaton/AutomatonTest.java b/src/test/java/io/github/contractautomata/catlib/automaton/AutomatonTest.java index a4b0aa82..35caf9b3 100644 --- a/src/test/java/io/github/contractautomata/catlib/automaton/AutomatonTest.java +++ b/src/test/java/io/github/contractautomata/catlib/automaton/AutomatonTest.java @@ -147,7 +147,8 @@ public void teardown() { public void testString() { String test = "Rank: 1"+System.lineSeparator() + "Initial state: [0]"+System.lineSeparator() + - "Final states: [[1, 2]]"+System.lineSeparator() + + "Final states: [[1, 2]]"+System.lineSeparator() + + "Committed states: [[]]" + System.lineSeparator() + "Transitions: "+System.lineSeparator() + "([0],[m],[1])"+System.lineSeparator() + "([0],[m],[2])"+System.lineSeparator(); @@ -244,7 +245,8 @@ public void testGetBasicStates() { public void testPrintFinalStates() { String test = "Rank: 2" + System.lineSeparator()+ "Initial state: [0, 0]" + System.lineSeparator()+ - "Final states: [[1][2]]" + System.lineSeparator()+ + "Final states: [[1][2]]" + System.lineSeparator()+ + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator()+ "!L([1, 2],[!test,?test],[0, 0])" + System.lineSeparator()+ "!U([0, 0],[!test,?test],[1, 0])" + System.lineSeparator()+ diff --git a/src/test/java/io/github/contractautomata/catlib/family/FMCATest.java b/src/test/java/io/github/contractautomata/catlib/family/FMCATest.java index 65279f85..be45dcc2 100644 --- a/src/test/java/io/github/contractautomata/catlib/family/FMCATest.java +++ b/src/test/java/io/github/contractautomata/catlib/family/FMCATest.java @@ -292,6 +292,7 @@ public void testGetCanonicalProducts() { String test1 = "[p2=Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[1][2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!f1,?f1],[1, 0])" + System.lineSeparator() + "([1, 0],[!f2,?f2],[1, 2])" + System.lineSeparator() + @@ -299,6 +300,7 @@ public void testGetCanonicalProducts() { String test2 = "=Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[1][2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!f1,?f1],[1, 0])" + System.lineSeparator() + "([1, 0],[!f2,?f2],[1, 2])" + System.lineSeparator() + @@ -324,6 +326,7 @@ public void testGetOrchestrationOfFamilyEnumerative() { String test = "Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[0_1][0_2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!dummy, -],[0_0, 0_0])" + System.lineSeparator() + "([0_0, 0_0],[!f1, ?f1],[0_1, 0_0])" + System.lineSeparator() + @@ -339,6 +342,7 @@ public void testGetOrchestrationOfFamily() { String test1 = "Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[0_1, 1_1][0_2, 1_2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!dummy, -],[0_0, 0_0])" + System.lineSeparator() + "([0, 0],[!dummy, -],[1_0, 1_0])" + System.lineSeparator() + @@ -351,6 +355,7 @@ public void testGetOrchestrationOfFamily() { String test2 = "Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[0_1, 1_1][0_2, 1_2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!dummy, -],[0_0, 0_0])" + System.lineSeparator() + "([0, 0],[!dummy, -],[1_0, 1_0])" + System.lineSeparator() + @@ -370,6 +375,7 @@ public void testGetTotalProductsWithNonemptyOrchestration() { String test = "{p4=Rank: 2" + System.lineSeparator() + "Initial state: [0, 0]" + System.lineSeparator() + "Final states: [[1][2]]" + System.lineSeparator() + + "Committed states: [[][]]" + System.lineSeparator() + "Transitions: " + System.lineSeparator() + "([0, 0],[!f1,?f1],[1, 0])" + System.lineSeparator() + "([1, 0],[!f2,?f2],[1, 2])" + System.lineSeparator() + diff --git a/src/test/java/it/io/github/contractautomata/catlib/automaton/ITAutomatonTest.java b/src/test/java/it/io/github/contractautomata/catlib/automaton/ITAutomatonTest.java index a8566603..efdf5cc6 100644 --- a/src/test/java/it/io/github/contractautomata/catlib/automaton/ITAutomatonTest.java +++ b/src/test/java/it/io/github/contractautomata/catlib/automaton/ITAutomatonTest.java @@ -46,6 +46,7 @@ public void testString() { String test = "Rank: 1"+System.lineSeparator() + "Initial state: [0]"+System.lineSeparator() + "Final states: [[1, 2]]"+System.lineSeparator() + + "Committed states: [[]]" + System.lineSeparator() + "Transitions: "+System.lineSeparator() + "([0],[m],[1])"+System.lineSeparator() + "([0],[m],[2])"+System.lineSeparator(); @@ -160,6 +161,7 @@ public void testToString() throws IOException { String test ="Rank: 3"+System.lineSeparator()+ "Initial state: [0, 0, 0]"+System.lineSeparator()+ "Final states: [[3][3][3]]"+System.lineSeparator()+ + "Committed states: [[][][]]" + System.lineSeparator() + "Transitions: "+System.lineSeparator()+ "!L([2, 9, 0],[?invoice, !invoice, -],[3, 3, 0])"+System.lineSeparator()+ "!L([3, 3, 0],[-, !singleRoom, ?singleRoom],[3, 6, 7])"+System.lineSeparator()+ diff --git a/src/test/java/it/io/github/contractautomata/catlib/encoders/ITDkBricksEncoderTest.java b/src/test/java/it/io/github/contractautomata/catlib/encoders/ITDkBricksEncoderTest.java new file mode 100644 index 00000000..c79b83ac --- /dev/null +++ b/src/test/java/it/io/github/contractautomata/catlib/encoders/ITDkBricksEncoderTest.java @@ -0,0 +1,67 @@ +package it.io.github.contractautomata.catlib.encoders; + +import io.github.contractautomata.catlib.automaton.label.CALabel; +import io.github.contractautomata.catlib.converters.AutDataConverter; + + +public class ITDkBricksEncoderTest { + private final AutDataConverter bdc = new AutDataConverter<>(CALabel::new); +// +// @Test +// public void test1() throws IOException { +// Automaton,ModalTransition,CALabel>> aut = bdc.importMSCA(ITAutomatonTest.dir + "NewOrc_(DealerxPlayerxPlayer).data"); +// DkBricsEncoder dbe = new DkBricsEncoder(aut); +// dk.brics.automaton.Automaton a = dbe.getDkAut(); +// System.out.println(a.getNumberOfTransitions() + " " + a.getNumberOfStates()); +// +// boolean isDeterministic = aut.getTransition().parallelStream() +// .noneMatch(t->aut.getTransition().parallelStream() +// .filter(tt->tt!=t) +// .noneMatch(tt->t.getSource().equals(tt.getSource()) && t.getLabel().equals(tt.getLabel()))); +// +// boolean isDkDeterministic = a.getStates().parallelStream() +// .anyMatch(s->s.getTransitions() +// .stream().map(Transition::getMin) +// .count()>1); +// +// System.out.println(isDkDeterministic + " " + isDeterministic); +// a.determinize(); +// +// System.out.println(a.getNumberOfTransitions() + " " + a.getNumberOfStates()); +// //System.out.println(a); +// //System.out.println(dbe.getCA()); +// assertTrue(AutomatonTest.autEquals(aut, dbe.getCA())); +// +// } +// +// +// @Test +// public void test2() throws IOException { +// BasicState bs0 = new BasicState<>("0",true,false); +// BasicState bs1 = new BasicState<>("1",false,true); +// BasicState bs2 = new BasicState<>("2",false,true); +// State cs0 = new State<>(List.of(bs0)); +// State cs1 = new State<>(List.of(bs1)); +// State cs2 = new State<>(List.of(bs2)); +// CALabel ca = new CALabel(List.of(new OfferAction("a"))); +// ModalTransition,CALabel> tr1 = new ModalTransition<>(cs0,ca,cs1, ModalTransition.Modality.PERMITTED); +// ModalTransition,CALabel> tr2 = new ModalTransition<>(cs0,ca,cs2, ModalTransition.Modality.PERMITTED); +// Automaton,ModalTransition,CALabel>> aut = new Automaton<>(Set.of(tr1,tr2)); +// +// DkBricsEncoder dbe = new DkBricsEncoder(aut); +// dk.brics.automaton.Automaton a = dbe.getDkAut(); +// System.out.println(a.toDot()); +// +// System.out.println("---------------------------------"); +// +// +//// dbe.getCA(); +// +// a.setDeterministic(false); +// a.determinize(); +// System.out.println(a.toDot()); +// System.out.println("---------------------------------"); +// +// assertTrue(AutomatonTest.autEquals(aut, dbe.getCA())); +// } +} diff --git a/src/test/java/it/io/github/contractautomata/catlib/operators/ITNewOrchestrationTest.java b/src/test/java/it/io/github/contractautomata/catlib/operators/ITNewOrchestrationTest.java index cfa96606..8796105d 100644 --- a/src/test/java/it/io/github/contractautomata/catlib/operators/ITNewOrchestrationTest.java +++ b/src/test/java/it/io/github/contractautomata/catlib/operators/ITNewOrchestrationTest.java @@ -3,26 +3,82 @@ import io.github.contractautomata.catlib.automaton.Automaton; import io.github.contractautomata.catlib.automaton.AutomatonTest; import io.github.contractautomata.catlib.automaton.label.CALabel; +import io.github.contractautomata.catlib.automaton.label.Label; import io.github.contractautomata.catlib.automaton.label.action.Action; +import io.github.contractautomata.catlib.automaton.state.BasicState; import io.github.contractautomata.catlib.automaton.state.State; import io.github.contractautomata.catlib.automaton.transition.ModalTransition; import io.github.contractautomata.catlib.converters.AutDataConverter; +import io.github.contractautomata.catlib.operations.MSCACompositionFunction; import io.github.contractautomata.catlib.operations.NewOrchestrationSynthesisOperator; import io.github.contractautomata.catlib.requirements.Agreement; +import io.github.contractautomata.catlib.requirements.StrongAgreement; import it.io.github.contractautomata.catlib.automaton.ITAutomatonTest; import org.junit.Before; import org.junit.Test; import java.io.IOException; -import java.util.Arrays; +import java.util.*; +import static org.junit.Assert.assertThrows; import static org.junit.Assert.assertTrue; public class ITNewOrchestrationTest { private final AutDataConverter bdc = new AutDataConverter<>(CALabel::new); - + private Automaton,ModalTransition,Label>> prop; @Before public void setup() { + BasicState s0 = new BasicState<>("WaitFirstCard", true, false); + BasicState s1 = new BasicState<>("WaitSecondCard", false, false); + BasicState s2 = new BasicState<>("Go", false, true); + State cs0 = new State<>(List.of(s0)); + State cs1 = new State<>(List.of(s1)); + State cs2 = new State<>(List.of(s2)); + + Set, Label>> setTr = new HashSet<>(); + setTr.add(new ModalTransition<>(cs0, new Label<>(List.of(new Action("pair1"))), cs1, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs0, new Label<>(List.of(new Action("pair2"))), cs1, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs0, new Label<>(List.of(new Action("pair3"))), cs1, ModalTransition.Modality.PERMITTED)); + + setTr.add(new ModalTransition<>(cs1, new Label<>(List.of(new Action("pair1"))), cs2, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs1, new Label<>(List.of(new Action("pair2"))), cs2, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs1, new Label<>(List.of(new Action("pair3"))), cs2, ModalTransition.Modality.PERMITTED)); + + + setTr.add(new ModalTransition<>(cs2, new Label<>(List.of(new Action("1"))), cs2, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs2, new Label<>(List.of(new Action("2"))), cs2, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs2, new Label<>(List.of(new Action("3"))), cs2, ModalTransition.Modality.PERMITTED)); + setTr.add(new ModalTransition<>(cs2, new Label<>(List.of(new Action("4"))), cs2, ModalTransition.Modality.PERMITTED)); + + prop = new Automaton<>(setTr); + } + + @Test + public void testOrcCardsGameICE2023modelcheck() throws IOException { + Automaton,ModalTransition,CALabel>> dealer = bdc.importMSCA(ITAutomatonTest.dir + "DealerNoCommitted.data"); + Automaton,ModalTransition,CALabel>> player = bdc.importMSCA(ITAutomatonTest.dir + "Player.data"); + + NewOrchestrationSynthesisOperator os = new NewOrchestrationSynthesisOperator(new StrongAgreement(),prop); + os.setIgnoreModality(); + Automaton,ModalTransition,CALabel>> orc = os.apply(List.of(dealer,player,player)); + + Automaton,ModalTransition,CALabel>> test = bdc.importMSCA(ITAutomatonTest.dir+ "NewOrc_(DealerxPlayerxPlayer)_modelcheck.data"); + + assertTrue(AutomatonTest.autEquals(orc, test)); + } + + @Test + public void testOrcCardsGameICE2023comp() throws IOException { + Automaton,ModalTransition,CALabel>> dealer = bdc.importMSCA(ITAutomatonTest.dir + "Dealer.data"); + Automaton,ModalTransition,CALabel>> player = bdc.importMSCA(ITAutomatonTest.dir + "Player.data"); + + Automaton,ModalTransition,CALabel>> comp = + new MSCACompositionFunction<>(List.of(dealer,player,player), t->new StrongAgreement().negate().test(t.getLabel()) ).apply(Integer.MAX_VALUE); + Automaton,ModalTransition,CALabel>> orc = new NewOrchestrationSynthesisOperator(new StrongAgreement()).apply(comp); + + //bdc.exportMSCA(ITAutomatonTest.dir+ "NewOrc_(DealerxPlayerxPlayer).data",orc); + Automaton,ModalTransition,CALabel>> test = bdc.importMSCA(ITAutomatonTest.dir+ "NewOrc_(DealerxPlayerxPlayer).data"); + assertTrue(AutomatonTest.autEquals(orc, test)); } @@ -30,10 +86,58 @@ public void setup() { public void testOrcCardsGameICE2023() throws IOException { Automaton,ModalTransition,CALabel>> dealer = bdc.importMSCA(ITAutomatonTest.dir + "Dealer.data"); Automaton,ModalTransition,CALabel>> player = bdc.importMSCA(ITAutomatonTest.dir + "Player.data"); - Automaton,ModalTransition,CALabel>> orc = new NewOrchestrationSynthesisOperator(new Agreement()).apply(Arrays.asList(dealer,player,player)); + Automaton,ModalTransition,CALabel>> orc = new NewOrchestrationSynthesisOperator(new StrongAgreement()).apply(List.of(dealer,player,player)); Automaton,ModalTransition,CALabel>> test = bdc.importMSCA(ITAutomatonTest.dir+ "NewOrc_(DealerxPlayerxPlayer).data"); assertTrue(AutomatonTest.autEquals(orc, test)); } -} \ No newline at end of file + + //------------EXCEPTIONS-------------- + + @Test + public void test_necessaryoffer_exception() throws Exception + { + Automaton,ModalTransition,CALabel>> aut = bdc.importMSCA(ITAutomatonTest.dir+ "PriviledgedClient.data"); + assertThrows("Some automaton contains necessary offers that are not allowed in the orchestration synthesis or some action is labelled with tau_", IllegalArgumentException.class, () -> new NewOrchestrationSynthesisOperator(new Agreement()).apply(List.of(aut))); + } + + @Test + public void test_onlyprincipals_exception() throws Exception + { + Automaton,ModalTransition,CALabel>> aut = bdc.importMSCA(ITAutomatonTest.dir+ "(AxB).data"); + assertThrows("Only principals are allowed", IllegalArgumentException.class, () -> new NewOrchestrationSynthesisOperator(new Agreement()).apply(List.of(aut))); + } + + + @Test + public void testExceptionTau() throws IOException { + Automaton,ModalTransition,CALabel>> player = bdc.importMSCA(ITAutomatonTest.dir + "PlayerEncoded.data"); + assertThrows("Some automaton contains necessary offers that are not allowed in the orchestration synthesis or some action is labelled with tau_",IllegalArgumentException.class,() -> new NewOrchestrationSynthesisOperator(new Agreement()).apply(List.of(player))); + + } + + +} + + +// @Test +// public void testEncoding() throws IOException { +// +// State s0 = new State<>(List.of( new BasicState<>("0",true,false), new BasicState<>("0",true,false))); +// State s1 = new State<>(List.of(new BasicState<>("1",false,false),new BasicState<>("1",false,false))); +// State s2 = new State<>(List.of(new BasicState<>("2",false,false),new BasicState<>("2",false,false))); +// State s3 = new State<>(List.of(new BasicState<>("3",false,true),new BasicState<>("3",false,true))); +// +// Set, CALabel>> setTr = new HashSet<>(); +// setTr.add(new ModalTransition<>(s0, new CALabel(List.of(new RequestAction("a"), new OfferAction("a"))), s1, ModalTransition.Modality.LAZY)); +// setTr.add(new ModalTransition<>(s0, new CALabel(List.of(new RequestAction("b"), new OfferAction("b"))), s2, ModalTransition.Modality.LAZY)); +// setTr.add(new ModalTransition<>(s2, new CALabel(List.of(new OfferAction("e"), new RequestAction("e"))), s1, ModalTransition.Modality.LAZY)); +// setTr.add(new ModalTransition<>(s1, new CALabel(List.of(new RequestAction("c"), new OfferAction("c"))), s3, ModalTransition.Modality.LAZY)); +// setTr.add(new ModalTransition<>(s2, new CALabel(List.of(new RequestAction("d"), new OfferAction("d"))), s3, ModalTransition.Modality.LAZY)); +// +// Automaton,ModalTransition,CALabel>> aut = new Automaton<>(setTr); +// +// // bdc.exportMSCA("test.data", new NewOrchestrationSynthesisOperator(new StrongAgreement()).apply(aut)); +// +// } \ No newline at end of file diff --git a/src/test/resources/(AxB).data b/src/test/resources/(AxB).data index b8bbd200..1ea89c4b 100644 --- a/src/test/resources/(AxB).data +++ b/src/test/resources/(AxB).data @@ -1,6 +1,7 @@ Rank: 2 Initial state: [0, 0] Final states: [[2][2]] +Committed states: [[][]] Transitions: ([0, 0],[!pippo, ?pippo],[1, 1]) ([1, 1],[-, !pluto],[1, 2]) diff --git a/src/test/resources/(BusinessClientxHotelxEconomyClient).data b/src/test/resources/(BusinessClientxHotelxEconomyClient).data index 969c77e6..e60c5779 100644 --- a/src/test/resources/(BusinessClientxHotelxEconomyClient).data +++ b/src/test/resources/(BusinessClientxHotelxEconomyClient).data @@ -1,6 +1,7 @@ Rank: 3 Initial state: [0, 0, 0] Final states: [[3][3][3]] +Committed states: [[][][]] Transitions: ([9, 3, 1],[-, !singleRoom, -],[9, 6, 1]) ([9, 2, 3],[-, !invoice, -],[9, 7, 3]) diff --git a/src/test/resources/BusinessClientxHotelxEconomyClient.data b/src/test/resources/BusinessClientxHotelxEconomyClient.data index 80776e88..bebfff2c 100644 --- a/src/test/resources/BusinessClientxHotelxEconomyClient.data +++ b/src/test/resources/BusinessClientxHotelxEconomyClient.data @@ -1,6 +1,7 @@ Rank: 3 Initial state: [0, 0, 0] Final states: [[3][3][3]] +Committed states: [[][][]] Transitions: !L([0, 0, 0],[-, !singleRoom, ?singleRoom],[0, 6, 7]) !L([0, 1, 2],[-, -, ?invoice],[0, 1, 3]) diff --git a/src/test/resources/BusinessClientxHotelxEconomyClient_export.data b/src/test/resources/BusinessClientxHotelxEconomyClient_export.data index 80776e88..bebfff2c 100644 --- a/src/test/resources/BusinessClientxHotelxEconomyClient_export.data +++ b/src/test/resources/BusinessClientxHotelxEconomyClient_export.data @@ -1,6 +1,7 @@ Rank: 3 Initial state: [0, 0, 0] Final states: [[3][3][3]] +Committed states: [[][][]] Transitions: !L([0, 0, 0],[-, !singleRoom, ?singleRoom],[0, 6, 7]) !L([0, 1, 2],[-, -, ?invoice],[0, 1, 3]) diff --git a/src/test/resources/Dealer.data b/src/test/resources/Dealer.data index 7044618d..416c956c 100644 --- a/src/test/resources/Dealer.data +++ b/src/test/resources/Dealer.data @@ -1,18 +1,23 @@ Rank: 1 Initial state: [Dealing] -Final states: [[Cards31, Cards32, Cards21, Cards41,Cards42,Cards43]] +Final states: [[Cards21, Cards31, Cards32, Cards41, Cards42, Cards43]] +Committed states: [[P1,P2,P3]] Transitions: -([Dealing],[?pair1],[P1]) -([Dealing],[?pair2],[P2]) -([P1],[?pair2],[Collecting]) -([P1],[?pair3],[Collecting]) -([P2],[?pair3],[Collecting]) -([Collecting],[!2],[Card2]) -([Collecting],[!3],[Card3]) -([Collecting],[!4],[Card4]) +([3],[!2],[Card2]) +([3],[!3],[Card3]) +([3],[!4],[Card4]) ([Card2],[!1],[Cards21]) -([Card3],[!2],[Cards32]) ([Card3],[!1],[Cards31]) +([Card3],[!2],[Cards32]) ([Card4],[!1],[Cards41]) ([Card4],[!2],[Cards42]) -([Card4],[!3],[Cards43]) \ No newline at end of file +([Card4],[!3],[Cards43]) +([Dealing],[?pair1],[P1]) +([Dealing],[?pair2],[P2]) +([Dealing],[?pair3],[P3]) +([P1],[?pair2],[3]) +([P1],[?pair3],[3]) +([P2],[?pair1],[3]) +([P2],[?pair3],[3]) +([P3],[?pair1],[3]) +([P3],[?pair2],[3]) diff --git a/src/test/resources/DealerNoCommitted.data b/src/test/resources/DealerNoCommitted.data new file mode 100644 index 00000000..787e5d6d --- /dev/null +++ b/src/test/resources/DealerNoCommitted.data @@ -0,0 +1,23 @@ +Rank: 1 +Initial state: [Dealing] +Final states: [[Cards21, Cards31, Cards32, Cards41, Cards42, Cards43]] +Committed states: [[]] +Transitions: +([3],[!2],[Card2]) +([3],[!3],[Card3]) +([3],[!4],[Card4]) +([Card2],[!1],[Cards21]) +([Card3],[!1],[Cards31]) +([Card3],[!2],[Cards32]) +([Card4],[!1],[Cards41]) +([Card4],[!2],[Cards42]) +([Card4],[!3],[Cards43]) +([Dealing],[?pair1],[P1]) +([Dealing],[?pair2],[P2]) +([Dealing],[?pair3],[P3]) +([P1],[?pair2],[3]) +([P1],[?pair3],[3]) +([P2],[?pair1],[3]) +([P2],[?pair3],[3]) +([P3],[?pair1],[3]) +([P3],[?pair2],[3]) diff --git a/src/test/resources/NewOrc_(DealerxPlayerxPlayer).data b/src/test/resources/NewOrc_(DealerxPlayerxPlayer).data index d83f9032..fdebf9ac 100644 --- a/src/test/resources/NewOrc_(DealerxPlayerxPlayer).data +++ b/src/test/resources/NewOrc_(DealerxPlayerxPlayer).data @@ -1,52 +1,59 @@ Rank: 3 Initial state: [Dealing, Waiting, Waiting] -Final states: [[Cards21, Cards31, Cards32, Cards41, Cards43][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3]] +Final states: [[Cards21, Cards32, Cards41, Cards43][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4]] +Committed states: [[P1, P2][][]] Transitions: -!L([Card2, Pair1_1_Pair1Card1, Pair2Card2],[!1, ?1, -],[Cards21, Pair1Card1, Pair2Card2]) -!L([Card2, Pair1_1_Pair1Card1, Pair3Card2],[!1, ?1, -],[Cards21, Pair1Card1, Pair3Card2]) -!L([Card2, Pair2Card2, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards21, Pair2Card2, Pair1Card1]) -!L([Card2, Pair3Card2, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards21, Pair3Card2, Pair1Card1]) -!L([Card3, Pair1Card3, Pair2_2_Pair2Card2],[!2, -, ?2],[Cards32, Pair1Card3, Pair2Card2]) -!L([Card3, Pair1_1_Pair1Card1, Pair3Card3],[!1, ?1, -],[Cards31, Pair1Card1, Pair3Card3]) -!L([Card3, Pair2_2_Pair2Card2, Pair1Card3],[!2, ?2, -],[Cards32, Pair2Card2, Pair1Card3]) -!L([Card3, Pair3Card3, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards31, Pair3Card3, Pair1Card1]) -!L([Card4, Pair1, Pair2Card4],[!1, ?1, -],[Cards41, Pair1Card1, Pair2Card4]) -!L([Card4, Pair1, Pair2Card4],[!3, ?3, -],[Cards43, Pair1Card3, Pair2Card4]) -!L([Card4, Pair1_1_Pair1Card1, Pair2Card4],[!1, ?1, -],[Cards41, Pair1Card1, Pair2Card4]) -!L([Card4, Pair1_3_Pair1Card3, Pair2Card4],[!3, ?3, -],[Cards43, Pair1Card3, Pair2Card4]) -!L([Card4, Pair2Card4, Pair1],[!1, -, ?1],[Cards41, Pair2Card4, Pair1Card1]) -!L([Card4, Pair2Card4, Pair1],[!3, -, ?3],[Cards43, Pair2Card4, Pair1Card3]) -!L([Card4, Pair2Card4, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards41, Pair2Card4, Pair1Card1]) -!L([Card4, Pair2Card4, Pair1_3_Pair1Card3],[!3, -, ?3],[Cards43, Pair2Card4, Pair1Card3]) -!L([Collecting, Pair1, Pair2],[!2, -, ?2],[Card2, Pair1_1_Pair1Card1, Pair2Card2]) -!L([Collecting, Pair1, Pair2],[!3, ?3, -],[Card3, Pair1Card3, Pair2_2_Pair2Card2]) -!L([Collecting, Pair1, Pair2],[!4, -, ?4],[Card4, Pair1, Pair2Card4]) -!L([Collecting, Pair1, Pair2],[!4, -, ?4],[Card4, Pair1_1_Pair1Card1, Pair2Card4]) -!L([Collecting, Pair1, Pair2],[!4, -, ?4],[Card4, Pair1_3_Pair1Card3, Pair2Card4]) -!L([Collecting, Pair1_1_Pair1Card1, Pair2],[!2, -, ?2],[Card2, Pair1_1_Pair1Card1, Pair2Card2]) -!L([Collecting, Pair1_1_Pair1Card1, Pair2],[!4, -, ?4],[Card4, Pair1_1_Pair1Card1, Pair2Card4]) -!L([Collecting, Pair1_1_Pair1Card1, Pair3],[!2, -, ?2],[Card2, Pair1_1_Pair1Card1, Pair3Card2]) -!L([Collecting, Pair1_1_Pair1Card1, Pair3],[!3, -, ?3],[Card3, Pair1_1_Pair1Card1, Pair3Card3]) -!L([Collecting, Pair1_3_Pair1Card3, Pair2],[!3, ?3, -],[Card3, Pair1Card3, Pair2_2_Pair2Card2]) -!L([Collecting, Pair1_3_Pair1Card3, Pair2],[!4, -, ?4],[Card4, Pair1_3_Pair1Card3, Pair2Card4]) -!L([Collecting, Pair2, Pair1],[!2, ?2, -],[Card2, Pair2Card2, Pair1_1_Pair1Card1]) -!L([Collecting, Pair2, Pair1],[!3, -, ?3],[Card3, Pair2_2_Pair2Card2, Pair1Card3]) -!L([Collecting, Pair2, Pair1],[!4, ?4, -],[Card4, Pair2Card4, Pair1]) -!L([Collecting, Pair2, Pair1],[!4, ?4, -],[Card4, Pair2Card4, Pair1_1_Pair1Card1]) -!L([Collecting, Pair2, Pair1],[!4, ?4, -],[Card4, Pair2Card4, Pair1_3_Pair1Card3]) -!L([Collecting, Pair2, Pair1_1_Pair1Card1],[!2, ?2, -],[Card2, Pair2Card2, Pair1_1_Pair1Card1]) -!L([Collecting, Pair2, Pair1_1_Pair1Card1],[!4, ?4, -],[Card4, Pair2Card4, Pair1_1_Pair1Card1]) -!L([Collecting, Pair2, Pair1_3_Pair1Card3],[!3, -, ?3],[Card3, Pair2_2_Pair2Card2, Pair1Card3]) -!L([Collecting, Pair2, Pair1_3_Pair1Card3],[!4, ?4, -],[Card4, Pair2Card4, Pair1_3_Pair1Card3]) -!L([Collecting, Pair3, Pair1_1_Pair1Card1],[!2, ?2, -],[Card2, Pair3Card2, Pair1_1_Pair1Card1]) -!L([Collecting, Pair3, Pair1_1_Pair1Card1],[!3, ?3, -],[Card3, Pair3Card3, Pair1_1_Pair1Card1]) +!U([3, Pair1, Pair2],[-, -, tau_2],[3, Pair1, Pair2_2_Pair2Card2]) +!U([3, Pair1, Pair2],[-, -, tau_4],[3, Pair1, Pair2_4_Pair2Card4]) +!U([3, Pair1, Pair2],[-, tau_1, -],[3, Pair1_1_Pair1Card1, Pair2]) +!U([3, Pair1, Pair2],[-, tau_3, -],[3, Pair1_3_Pair1Card3, Pair2]) +!U([3, Pair1, Pair2_2_Pair2Card2],[-, tau_1, -],[3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2]) +!U([3, Pair1, Pair2_2_Pair2Card2],[-, tau_3, -],[3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2]) +!U([3, Pair1, Pair2_4_Pair2Card4],[-, tau_1, -],[3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4]) +!U([3, Pair1, Pair2_4_Pair2Card4],[-, tau_3, -],[3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4]) +!U([3, Pair1_1_Pair1Card1, Pair2],[-, -, tau_2],[3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2]) +!U([3, Pair1_1_Pair1Card1, Pair2],[-, -, tau_4],[3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4]) +!U([3, Pair1_3_Pair1Card3, Pair2],[-, -, tau_2],[3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2]) +!U([3, Pair1_3_Pair1Card3, Pair2],[-, -, tau_4],[3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4]) +!U([3, Pair2, Pair1],[-, -, tau_1],[3, Pair2, Pair1_1_Pair1Card1]) +!U([3, Pair2, Pair1],[-, -, tau_3],[3, Pair2, Pair1_3_Pair1Card3]) +!U([3, Pair2, Pair1],[-, tau_2, -],[3, Pair2_2_Pair2Card2, Pair1]) +!U([3, Pair2, Pair1],[-, tau_4, -],[3, Pair2_4_Pair2Card4, Pair1]) +!U([3, Pair2, Pair1_1_Pair1Card1],[-, tau_2, -],[3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1]) +!U([3, Pair2, Pair1_1_Pair1Card1],[-, tau_4, -],[3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1]) +!U([3, Pair2, Pair1_3_Pair1Card3],[-, tau_2, -],[3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3]) +!U([3, Pair2, Pair1_3_Pair1Card3],[-, tau_4, -],[3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3]) +!U([3, Pair2_2_Pair2Card2, Pair1],[-, -, tau_1],[3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1]) +!U([3, Pair2_2_Pair2Card2, Pair1],[-, -, tau_3],[3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3]) +!U([3, Pair2_4_Pair2Card4, Pair1],[-, -, tau_1],[3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1]) +!U([3, Pair2_4_Pair2Card4, Pair1],[-, -, tau_3],[3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3]) +!U([Card4, Pair1, Pair2Card4],[-, tau_1, -],[Card4, Pair1_1_Pair1Card1, Pair2Card4]) +!U([Card4, Pair1, Pair2Card4],[-, tau_3, -],[Card4, Pair1_3_Pair1Card3, Pair2Card4]) +!U([Card4, Pair2Card4, Pair1],[-, -, tau_1],[Card4, Pair2Card4, Pair1_1_Pair1Card1]) +!U([Card4, Pair2Card4, Pair1],[-, -, tau_3],[Card4, Pair2Card4, Pair1_3_Pair1Card3]) +([3, Pair1, Pair2_4_Pair2Card4],[!4, -, ?4],[Card4, Pair1, Pair2Card4]) +([3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2],[!2, -, ?2],[Card2, Pair1_1_Pair1Card1, Pair2Card2]) +([3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4],[!4, -, ?4],[Card4, Pair1_1_Pair1Card1, Pair2Card4]) +([3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2],[!3, ?3, -],[Card3, Pair1Card3, Pair2_2_Pair2Card2]) +([3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4],[!4, -, ?4],[Card4, Pair1_3_Pair1Card3, Pair2Card4]) +([3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1],[!2, ?2, -],[Card2, Pair2Card2, Pair1_1_Pair1Card1]) +([3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3],[!3, -, ?3],[Card3, Pair2_2_Pair2Card2, Pair1Card3]) +([3, Pair2_4_Pair2Card4, Pair1],[!4, ?4, -],[Card4, Pair2Card4, Pair1]) +([3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1],[!4, ?4, -],[Card4, Pair2Card4, Pair1_1_Pair1Card1]) +([3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3],[!4, ?4, -],[Card4, Pair2Card4, Pair1_3_Pair1Card3]) +([Card2, Pair1_1_Pair1Card1, Pair2Card2],[!1, ?1, -],[Cards21, Pair1Card1, Pair2Card2]) +([Card2, Pair2Card2, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards21, Pair2Card2, Pair1Card1]) +([Card3, Pair1Card3, Pair2_2_Pair2Card2],[!2, -, ?2],[Cards32, Pair1Card3, Pair2Card2]) +([Card3, Pair2_2_Pair2Card2, Pair1Card3],[!2, ?2, -],[Cards32, Pair2Card2, Pair1Card3]) +([Card4, Pair1_1_Pair1Card1, Pair2Card4],[!1, ?1, -],[Cards41, Pair1Card1, Pair2Card4]) +([Card4, Pair1_3_Pair1Card3, Pair2Card4],[!3, ?3, -],[Cards43, Pair1Card3, Pair2Card4]) +([Card4, Pair2Card4, Pair1_1_Pair1Card1],[!1, -, ?1],[Cards41, Pair2Card4, Pair1Card1]) +([Card4, Pair2Card4, Pair1_3_Pair1Card3],[!3, -, ?3],[Cards43, Pair2Card4, Pair1Card3]) ([Dealing, Waiting, Waiting],[?pair1, !pair1, -],[P1, Pair1, Waiting]) ([Dealing, Waiting, Waiting],[?pair1, -, !pair1],[P1, Waiting, Pair1]) -([P1, Pair1, Waiting],[?pair2, -, !pair2],[Collecting, Pair1, Pair2]) -([P1, Pair1, Waiting],[?pair2, -, !pair2],[Collecting, Pair1_1_Pair1Card1, Pair2]) -([P1, Pair1, Waiting],[?pair2, -, !pair2],[Collecting, Pair1_3_Pair1Card3, Pair2]) -([P1, Pair1, Waiting],[?pair3, -, !pair3],[Collecting, Pair1_1_Pair1Card1, Pair3]) -([P1, Waiting, Pair1],[?pair2, !pair2, -],[Collecting, Pair2, Pair1]) -([P1, Waiting, Pair1],[?pair2, !pair2, -],[Collecting, Pair2, Pair1_1_Pair1Card1]) -([P1, Waiting, Pair1],[?pair2, !pair2, -],[Collecting, Pair2, Pair1_3_Pair1Card3]) -([P1, Waiting, Pair1],[?pair3, !pair3, -],[Collecting, Pair3, Pair1_1_Pair1Card1]) +([Dealing, Waiting, Waiting],[?pair2, !pair2, -],[P2, Pair2, Waiting]) +([Dealing, Waiting, Waiting],[?pair2, -, !pair2],[P2, Waiting, Pair2]) +([P1, Pair1, Waiting],[?pair2, -, !pair2],[3, Pair1, Pair2]) +([P1, Waiting, Pair1],[?pair2, !pair2, -],[3, Pair2, Pair1]) +([P2, Pair2, Waiting],[?pair1, -, !pair1],[3, Pair2, Pair1]) +([P2, Waiting, Pair2],[?pair1, !pair1, -],[3, Pair1, Pair2]) diff --git a/src/test/resources/NewOrc_(DealerxPlayerxPlayer)_modelcheck.data b/src/test/resources/NewOrc_(DealerxPlayerxPlayer)_modelcheck.data new file mode 100644 index 00000000..6b2e01f0 --- /dev/null +++ b/src/test/resources/NewOrc_(DealerxPlayerxPlayer)_modelcheck.data @@ -0,0 +1,135 @@ +Rank: 4 +Initial state: [Dealing, Waiting, Waiting, WaitFirstCard] +Final states: [[Cards21, Cards31, Cards32, Cards41, Cards42, Cards43][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3][Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3][Go]] +Committed states: [[][][][]] +Transitions: +!U([3, Pair1, Pair2, Go],[-, -, tau_2, -],[3, Pair1, Pair2_2_Pair2Card2, Go]) +!U([3, Pair1, Pair2, Go],[-, -, tau_4, -],[3, Pair1, Pair2_4_Pair2Card4, Go]) +!U([3, Pair1, Pair2, Go],[-, tau_1, -, -],[3, Pair1_1_Pair1Card1, Pair2, Go]) +!U([3, Pair1, Pair2, Go],[-, tau_3, -, -],[3, Pair1_3_Pair1Card3, Pair2, Go]) +!U([3, Pair1, Pair2_2_Pair2Card2, Go],[-, tau_1, -, -],[3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2, Go]) +!U([3, Pair1, Pair2_2_Pair2Card2, Go],[-, tau_3, -, -],[3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2, Go]) +!U([3, Pair1, Pair2_4_Pair2Card4, Go],[-, tau_1, -, -],[3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4, Go]) +!U([3, Pair1, Pair2_4_Pair2Card4, Go],[-, tau_3, -, -],[3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4, Go]) +!U([3, Pair1, Pair3_2_Pair3Card2, Go],[-, tau_1, -, -],[3, Pair1_1_Pair1Card1, Pair3_2_Pair3Card2, Go]) +!U([3, Pair1, Pair3_2_Pair3Card2, Go],[-, tau_3, -, -],[3, Pair1_3_Pair1Card3, Pair3_2_Pair3Card2, Go]) +!U([3, Pair1_1_Pair1Card1, Pair2, Go],[-, -, tau_2, -],[3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2, Go]) +!U([3, Pair1_1_Pair1Card1, Pair2, Go],[-, -, tau_4, -],[3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4, Go]) +!U([3, Pair1_1_Pair1Card1, Pair3, Go],[-, -, tau_2, -],[3, Pair1_1_Pair1Card1, Pair3_2_Pair3Card2, Go]) +!U([3, Pair1_1_Pair1Card1, Pair3, Go],[-, -, tau_3, -],[3, Pair1_1_Pair1Card1, Pair3_3_Pair3Card3, Go]) +!U([3, Pair1_3_Pair1Card3, Pair2, Go],[-, -, tau_2, -],[3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2, Go]) +!U([3, Pair1_3_Pair1Card3, Pair2, Go],[-, -, tau_4, -],[3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4, Go]) +!U([3, Pair2, Pair1, Go],[-, -, tau_1, -],[3, Pair2, Pair1_1_Pair1Card1, Go]) +!U([3, Pair2, Pair1, Go],[-, -, tau_3, -],[3, Pair2, Pair1_3_Pair1Card3, Go]) +!U([3, Pair2, Pair1, Go],[-, tau_2, -, -],[3, Pair2_2_Pair2Card2, Pair1, Go]) +!U([3, Pair2, Pair1, Go],[-, tau_4, -, -],[3, Pair2_4_Pair2Card4, Pair1, Go]) +!U([3, Pair2, Pair1_1_Pair1Card1, Go],[-, tau_2, -, -],[3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1, Go]) +!U([3, Pair2, Pair1_1_Pair1Card1, Go],[-, tau_4, -, -],[3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1, Go]) +!U([3, Pair2, Pair1_3_Pair1Card3, Go],[-, tau_2, -, -],[3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3, Go]) +!U([3, Pair2, Pair1_3_Pair1Card3, Go],[-, tau_4, -, -],[3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3, Go]) +!U([3, Pair2, Pair3_3_Pair3Card3, Go],[-, tau_2, -, -],[3, Pair2_2_Pair2Card2, Pair3_3_Pair3Card3, Go]) +!U([3, Pair2, Pair3_3_Pair3Card3, Go],[-, tau_4, -, -],[3, Pair2_4_Pair2Card4, Pair3_3_Pair3Card3, Go]) +!U([3, Pair2_2_Pair2Card2, Pair1, Go],[-, -, tau_1, -],[3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1, Go]) +!U([3, Pair2_2_Pair2Card2, Pair1, Go],[-, -, tau_3, -],[3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3, Go]) +!U([3, Pair2_4_Pair2Card4, Pair1, Go],[-, -, tau_1, -],[3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1, Go]) +!U([3, Pair2_4_Pair2Card4, Pair1, Go],[-, -, tau_3, -],[3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3, Go]) +!U([3, Pair2_4_Pair2Card4, Pair3, Go],[-, -, tau_2, -],[3, Pair2_4_Pair2Card4, Pair3_2_Pair3Card2, Go]) +!U([3, Pair2_4_Pair2Card4, Pair3, Go],[-, -, tau_3, -],[3, Pair2_4_Pair2Card4, Pair3_3_Pair3Card3, Go]) +!U([3, Pair3, Pair1_1_Pair1Card1, Go],[-, tau_2, -, -],[3, Pair3_2_Pair3Card2, Pair1_1_Pair1Card1, Go]) +!U([3, Pair3, Pair1_1_Pair1Card1, Go],[-, tau_3, -, -],[3, Pair3_3_Pair3Card3, Pair1_1_Pair1Card1, Go]) +!U([3, Pair3, Pair2_4_Pair2Card4, Go],[-, tau_2, -, -],[3, Pair3_2_Pair3Card2, Pair2_4_Pair2Card4, Go]) +!U([3, Pair3, Pair2_4_Pair2Card4, Go],[-, tau_3, -, -],[3, Pair3_3_Pair3Card3, Pair2_4_Pair2Card4, Go]) +!U([3, Pair3_2_Pair3Card2, Pair1, Go],[-, -, tau_1, -],[3, Pair3_2_Pair3Card2, Pair1_1_Pair1Card1, Go]) +!U([3, Pair3_2_Pair3Card2, Pair1, Go],[-, -, tau_3, -],[3, Pair3_2_Pair3Card2, Pair1_3_Pair1Card3, Go]) +!U([3, Pair3_3_Pair3Card3, Pair2, Go],[-, -, tau_2, -],[3, Pair3_3_Pair3Card3, Pair2_2_Pair2Card2, Go]) +!U([3, Pair3_3_Pair3Card3, Pair2, Go],[-, -, tau_4, -],[3, Pair3_3_Pair3Card3, Pair2_4_Pair2Card4, Go]) +!U([Card4, Pair1, Pair2Card4, Go],[-, tau_1, -, -],[Card4, Pair1_1_Pair1Card1, Pair2Card4, Go]) +!U([Card4, Pair1, Pair2Card4, Go],[-, tau_3, -, -],[Card4, Pair1_3_Pair1Card3, Pair2Card4, Go]) +!U([Card4, Pair2Card4, Pair1, Go],[-, -, tau_1, -],[Card4, Pair2Card4, Pair1_1_Pair1Card1, Go]) +!U([Card4, Pair2Card4, Pair1, Go],[-, -, tau_3, -],[Card4, Pair2Card4, Pair1_3_Pair1Card3, Go]) +!U([Card4, Pair2Card4, Pair3, Go],[-, -, tau_2, -],[Card4, Pair2Card4, Pair3_2_Pair3Card2, Go]) +!U([Card4, Pair2Card4, Pair3, Go],[-, -, tau_3, -],[Card4, Pair2Card4, Pair3_3_Pair3Card3, Go]) +!U([Card4, Pair3, Pair2Card4, Go],[-, tau_2, -, -],[Card4, Pair3_2_Pair3Card2, Pair2Card4, Go]) +!U([Card4, Pair3, Pair2Card4, Go],[-, tau_3, -, -],[Card4, Pair3_3_Pair3Card3, Pair2Card4, Go]) +!U([P1, Pair1, Waiting, WaitSecondCard],[-, tau_1, -, -],[P1, Pair1_1_Pair1Card1, Waiting, WaitSecondCard]) +!U([P1, Pair1, Waiting, WaitSecondCard],[-, tau_3, -, -],[P1, Pair1_3_Pair1Card3, Waiting, WaitSecondCard]) +!U([P1, Waiting, Pair1, WaitSecondCard],[-, -, tau_1, -],[P1, Waiting, Pair1_1_Pair1Card1, WaitSecondCard]) +!U([P1, Waiting, Pair1, WaitSecondCard],[-, -, tau_3, -],[P1, Waiting, Pair1_3_Pair1Card3, WaitSecondCard]) +!U([P2, Pair2, Waiting, WaitSecondCard],[-, tau_2, -, -],[P2, Pair2_2_Pair2Card2, Waiting, WaitSecondCard]) +!U([P2, Pair2, Waiting, WaitSecondCard],[-, tau_4, -, -],[P2, Pair2_4_Pair2Card4, Waiting, WaitSecondCard]) +!U([P2, Waiting, Pair2, WaitSecondCard],[-, -, tau_2, -],[P2, Waiting, Pair2_2_Pair2Card2, WaitSecondCard]) +!U([P2, Waiting, Pair2, WaitSecondCard],[-, -, tau_4, -],[P2, Waiting, Pair2_4_Pair2Card4, WaitSecondCard]) +!U([P3, Pair3, Waiting, WaitSecondCard],[-, tau_2, -, -],[P3, Pair3_2_Pair3Card2, Waiting, WaitSecondCard]) +!U([P3, Pair3, Waiting, WaitSecondCard],[-, tau_3, -, -],[P3, Pair3_3_Pair3Card3, Waiting, WaitSecondCard]) +!U([P3, Waiting, Pair3, WaitSecondCard],[-, -, tau_2, -],[P3, Waiting, Pair3_2_Pair3Card2, WaitSecondCard]) +!U([P3, Waiting, Pair3, WaitSecondCard],[-, -, tau_3, -],[P3, Waiting, Pair3_3_Pair3Card3, WaitSecondCard]) +([3, Pair1, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair1, Pair2Card4, Go]) +([3, Pair1_1_Pair1Card1, Pair2_2_Pair2Card2, Go],[!2, -, ?2, -],[Card2, Pair1_1_Pair1Card1, Pair2Card2, Go]) +([3, Pair1_1_Pair1Card1, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair1_1_Pair1Card1, Pair2Card4, Go]) +([3, Pair1_1_Pair1Card1, Pair3_2_Pair3Card2, Go],[!2, -, ?2, -],[Card2, Pair1_1_Pair1Card1, Pair3Card2, Go]) +([3, Pair1_1_Pair1Card1, Pair3_3_Pair3Card3, Go],[!3, -, ?3, -],[Card3, Pair1_1_Pair1Card1, Pair3Card3, Go]) +([3, Pair1_3_Pair1Card3, Pair2_2_Pair2Card2, Go],[!3, ?3, -, -],[Card3, Pair1Card3, Pair2_2_Pair2Card2, Go]) +([3, Pair1_3_Pair1Card3, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair1_3_Pair1Card3, Pair2Card4, Go]) +([3, Pair1_3_Pair1Card3, Pair3_2_Pair3Card2, Go],[!3, ?3, -, -],[Card3, Pair1Card3, Pair3_2_Pair3Card2, Go]) +([3, Pair2_2_Pair2Card2, Pair1_1_Pair1Card1, Go],[!2, ?2, -, -],[Card2, Pair2Card2, Pair1_1_Pair1Card1, Go]) +([3, Pair2_2_Pair2Card2, Pair1_3_Pair1Card3, Go],[!3, -, ?3, -],[Card3, Pair2_2_Pair2Card2, Pair1Card3, Go]) +([3, Pair2_2_Pair2Card2, Pair3_3_Pair3Card3, Go],[!3, -, ?3, -],[Card3, Pair2_2_Pair2Card2, Pair3Card3, Go]) +([3, Pair2_4_Pair2Card4, Pair1, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair1, Go]) +([3, Pair2_4_Pair2Card4, Pair1_1_Pair1Card1, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair1_1_Pair1Card1, Go]) +([3, Pair2_4_Pair2Card4, Pair1_3_Pair1Card3, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair1_3_Pair1Card3, Go]) +([3, Pair2_4_Pair2Card4, Pair3, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair3, Go]) +([3, Pair2_4_Pair2Card4, Pair3_2_Pair3Card2, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair3_2_Pair3Card2, Go]) +([3, Pair2_4_Pair2Card4, Pair3_3_Pair3Card3, Go],[!4, ?4, -, -],[Card4, Pair2Card4, Pair3_3_Pair3Card3, Go]) +([3, Pair3, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair3, Pair2Card4, Go]) +([3, Pair3_2_Pair3Card2, Pair1_1_Pair1Card1, Go],[!2, ?2, -, -],[Card2, Pair3Card2, Pair1_1_Pair1Card1, Go]) +([3, Pair3_2_Pair3Card2, Pair1_3_Pair1Card3, Go],[!3, -, ?3, -],[Card3, Pair3_2_Pair3Card2, Pair1Card3, Go]) +([3, Pair3_2_Pair3Card2, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair3_2_Pair3Card2, Pair2Card4, Go]) +([3, Pair3_3_Pair3Card3, Pair1_1_Pair1Card1, Go],[!3, ?3, -, -],[Card3, Pair3Card3, Pair1_1_Pair1Card1, Go]) +([3, Pair3_3_Pair3Card3, Pair2_2_Pair2Card2, Go],[!3, ?3, -, -],[Card3, Pair3Card3, Pair2_2_Pair2Card2, Go]) +([3, Pair3_3_Pair3Card3, Pair2_4_Pair2Card4, Go],[!4, -, ?4, -],[Card4, Pair3_3_Pair3Card3, Pair2Card4, Go]) +([Card2, Pair1_1_Pair1Card1, Pair2Card2, Go],[!1, ?1, -, -],[Cards21, Pair1Card1, Pair2Card2, Go]) +([Card2, Pair1_1_Pair1Card1, Pair3Card2, Go],[!1, ?1, -, -],[Cards21, Pair1Card1, Pair3Card2, Go]) +([Card2, Pair2Card2, Pair1_1_Pair1Card1, Go],[!1, -, ?1, -],[Cards21, Pair2Card2, Pair1Card1, Go]) +([Card2, Pair3Card2, Pair1_1_Pair1Card1, Go],[!1, -, ?1, -],[Cards21, Pair3Card2, Pair1Card1, Go]) +([Card3, Pair1Card3, Pair2_2_Pair2Card2, Go],[!2, -, ?2, -],[Cards32, Pair1Card3, Pair2Card2, Go]) +([Card3, Pair1Card3, Pair3_2_Pair3Card2, Go],[!2, -, ?2, -],[Cards32, Pair1Card3, Pair3Card2, Go]) +([Card3, Pair1_1_Pair1Card1, Pair3Card3, Go],[!1, ?1, -, -],[Cards31, Pair1Card1, Pair3Card3, Go]) +([Card3, Pair2_2_Pair2Card2, Pair1Card3, Go],[!2, ?2, -, -],[Cards32, Pair2Card2, Pair1Card3, Go]) +([Card3, Pair2_2_Pair2Card2, Pair3Card3, Go],[!2, ?2, -, -],[Cards32, Pair2Card2, Pair3Card3, Go]) +([Card3, Pair3Card3, Pair1_1_Pair1Card1, Go],[!1, -, ?1, -],[Cards31, Pair3Card3, Pair1Card1, Go]) +([Card3, Pair3Card3, Pair2_2_Pair2Card2, Go],[!2, -, ?2, -],[Cards32, Pair3Card3, Pair2Card2, Go]) +([Card3, Pair3_2_Pair3Card2, Pair1Card3, Go],[!2, ?2, -, -],[Cards32, Pair3Card2, Pair1Card3, Go]) +([Card4, Pair1_1_Pair1Card1, Pair2Card4, Go],[!1, ?1, -, -],[Cards41, Pair1Card1, Pair2Card4, Go]) +([Card4, Pair1_3_Pair1Card3, Pair2Card4, Go],[!3, ?3, -, -],[Cards43, Pair1Card3, Pair2Card4, Go]) +([Card4, Pair2Card4, Pair1_1_Pair1Card1, Go],[!1, -, ?1, -],[Cards41, Pair2Card4, Pair1Card1, Go]) +([Card4, Pair2Card4, Pair1_3_Pair1Card3, Go],[!3, -, ?3, -],[Cards43, Pair2Card4, Pair1Card3, Go]) +([Card4, Pair2Card4, Pair3_2_Pair3Card2, Go],[!2, -, ?2, -],[Cards42, Pair2Card4, Pair3Card2, Go]) +([Card4, Pair2Card4, Pair3_3_Pair3Card3, Go],[!3, -, ?3, -],[Cards43, Pair2Card4, Pair3Card3, Go]) +([Card4, Pair3_2_Pair3Card2, Pair2Card4, Go],[!2, ?2, -, -],[Cards42, Pair3Card2, Pair2Card4, Go]) +([Card4, Pair3_3_Pair3Card3, Pair2Card4, Go],[!3, ?3, -, -],[Cards43, Pair3Card3, Pair2Card4, Go]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair1, !pair1, -, -],[P1, Pair1, Waiting, WaitSecondCard]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair1, -, !pair1, -],[P1, Waiting, Pair1, WaitSecondCard]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair2, !pair2, -, -],[P2, Pair2, Waiting, WaitSecondCard]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair2, -, !pair2, -],[P2, Waiting, Pair2, WaitSecondCard]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair3, !pair3, -, -],[P3, Pair3, Waiting, WaitSecondCard]) +([Dealing, Waiting, Waiting, WaitFirstCard],[?pair3, -, !pair3, -],[P3, Waiting, Pair3, WaitSecondCard]) +([P1, Pair1, Waiting, WaitSecondCard],[?pair2, -, !pair2, -],[3, Pair1, Pair2, Go]) +([P1, Pair1_1_Pair1Card1, Waiting, WaitSecondCard],[?pair2, -, !pair2, -],[3, Pair1_1_Pair1Card1, Pair2, Go]) +([P1, Pair1_1_Pair1Card1, Waiting, WaitSecondCard],[?pair3, -, !pair3, -],[3, Pair1_1_Pair1Card1, Pair3, Go]) +([P1, Pair1_3_Pair1Card3, Waiting, WaitSecondCard],[?pair2, -, !pair2, -],[3, Pair1_3_Pair1Card3, Pair2, Go]) +([P1, Waiting, Pair1, WaitSecondCard],[?pair2, !pair2, -, -],[3, Pair2, Pair1, Go]) +([P1, Waiting, Pair1_1_Pair1Card1, WaitSecondCard],[?pair2, !pair2, -, -],[3, Pair2, Pair1_1_Pair1Card1, Go]) +([P1, Waiting, Pair1_1_Pair1Card1, WaitSecondCard],[?pair3, !pair3, -, -],[3, Pair3, Pair1_1_Pair1Card1, Go]) +([P1, Waiting, Pair1_3_Pair1Card3, WaitSecondCard],[?pair2, !pair2, -, -],[3, Pair2, Pair1_3_Pair1Card3, Go]) +([P2, Pair2, Waiting, WaitSecondCard],[?pair1, -, !pair1, -],[3, Pair2, Pair1, Go]) +([P2, Pair2_2_Pair2Card2, Waiting, WaitSecondCard],[?pair1, -, !pair1, -],[3, Pair2_2_Pair2Card2, Pair1, Go]) +([P2, Pair2_4_Pair2Card4, Waiting, WaitSecondCard],[?pair1, -, !pair1, -],[3, Pair2_4_Pair2Card4, Pair1, Go]) +([P2, Pair2_4_Pair2Card4, Waiting, WaitSecondCard],[?pair3, -, !pair3, -],[3, Pair2_4_Pair2Card4, Pair3, Go]) +([P2, Waiting, Pair2, WaitSecondCard],[?pair1, !pair1, -, -],[3, Pair1, Pair2, Go]) +([P2, Waiting, Pair2_2_Pair2Card2, WaitSecondCard],[?pair1, !pair1, -, -],[3, Pair1, Pair2_2_Pair2Card2, Go]) +([P2, Waiting, Pair2_4_Pair2Card4, WaitSecondCard],[?pair1, !pair1, -, -],[3, Pair1, Pair2_4_Pair2Card4, Go]) +([P2, Waiting, Pair2_4_Pair2Card4, WaitSecondCard],[?pair3, !pair3, -, -],[3, Pair3, Pair2_4_Pair2Card4, Go]) +([P3, Pair3_2_Pair3Card2, Waiting, WaitSecondCard],[?pair1, -, !pair1, -],[3, Pair3_2_Pair3Card2, Pair1, Go]) +([P3, Pair3_3_Pair3Card3, Waiting, WaitSecondCard],[?pair2, -, !pair2, -],[3, Pair3_3_Pair3Card3, Pair2, Go]) +([P3, Waiting, Pair3_2_Pair3Card2, WaitSecondCard],[?pair1, !pair1, -, -],[3, Pair1, Pair3_2_Pair3Card2, Go]) +([P3, Waiting, Pair3_3_Pair3Card3, WaitSecondCard],[?pair2, !pair2, -, -],[3, Pair2, Pair3_3_Pair3Card3, Go]) diff --git a/src/test/resources/PlayerEncoded.data b/src/test/resources/PlayerEncoded.data new file mode 100644 index 00000000..1fb6bd69 --- /dev/null +++ b/src/test/resources/PlayerEncoded.data @@ -0,0 +1,19 @@ +Rank: 1 +Initial state: [Waiting] +Final states: [[Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3]] +Transitions: +!U([Pair1],[!tau1],[Pair1_1_Pair1Card1]) +!U([Pair1],[!tau3],[Pair1_3_Pair1Card3]) +!U([Pair2],[!tau2],[Pair2_2_Pair2Card2]) +!U([Pair2],[!tau4],[Pair2_4_Pair2Card4]) +!U([Pair3],[!tau2],[Pair3_2_Pair3Card2]) +!U([Pair3],[!tau3],[Pair3_3_Pair3Card3]) +([Pair1_1_Pair1Card1],[?1],[Pair1Card1]) +([Pair1_3_Pair1Card3],[?3],[Pair1Card3]) +([Pair2_2_Pair2Card2],[?2],[Pair2Card2]) +([Pair2_4_Pair2Card4],[?4],[Pair2Card4]) +([Pair3_2_Pair3Card2],[?2],[Pair3Card2]) +([Pair3_3_Pair3Card3],[?3],[Pair3Card3]) +([Waiting],[!pair1],[Pair1]) +([Waiting],[!pair2],[Pair2]) +([Waiting],[!pair3],[Pair3]) diff --git a/src/test/resources/testcor_concur21_Example34_closureCA.data b/src/test/resources/testcor_concur21_Example34_closureCA.data index eea32062..a2cb6928 100644 --- a/src/test/resources/testcor_concur21_Example34_closureCA.data +++ b/src/test/resources/testcor_concur21_Example34_closureCA.data @@ -1,6 +1,7 @@ Rank: 3 Initial state: [0, 0, 0] Final states: [[0, 1, 2, 3][0, 1, 2][0, 1, 2]] +Committed states: [[][][]] Transitions: ([0, 0, 0],[-, 2_1@?m, 2_1@!m],[0, 1, 1]) ([0, 0, 0],[0_1@!m, 0_1@?m, -],[3, 1, 0])