diff --git a/src/main/java/io/github/contractautomata/catlib/operations/SplittingOrchestrationSynthesisOperator.java b/src/main/java/io/github/contractautomata/catlib/operations/SplittingOrchestrationSynthesisOperator.java index 0f1c2eb5..8e3d2fa6 100644 --- a/src/main/java/io/github/contractautomata/catlib/operations/SplittingOrchestrationSynthesisOperator.java +++ b/src/main/java/io/github/contractautomata/catlib/operations/SplittingOrchestrationSynthesisOperator.java @@ -77,6 +77,9 @@ public Automaton,ModalTransition, ModalTransition, CALabel>> comp = new MSCACompositionFunction<>(encodePrincipals(laut), t->this.getReq().negate().test(t.getLabel()) || pruningPred.test(t)).apply(Integer.MAX_VALUE); + if (Objects.isNull(comp)) + return null; + //apply mpc synthesis to the encoded automata Automaton, ModalTransition, CALabel>> mpc = super.apply(comp); diff --git a/src/test/resources/Dealer.data b/src/test/resources/Dealer.data new file mode 100644 index 00000000..416c956c --- /dev/null +++ b/src/test/resources/Dealer.data @@ -0,0 +1,23 @@ +Rank: 1 +Initial state: [Dealing] +Final states: [[Cards21, Cards31, Cards32, Cards41, Cards42, Cards43]] +Committed states: [[P1,P2,P3]] +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/Player.data b/src/test/resources/Player.data new file mode 100644 index 00000000..ff6c871b --- /dev/null +++ b/src/test/resources/Player.data @@ -0,0 +1,13 @@ +Rank: 1 +Initial state: [Waiting] +Final states: [[Pair1Card1, Pair1Card3, Pair2Card2, Pair2Card4, Pair3Card2, Pair3Card3]] +Transitions: +!L([Pair1],[?1],[Pair1Card1]) +!L([Pair1],[?3],[Pair1Card3]) +!L([Pair2],[?2],[Pair2Card2]) +!L([Pair2],[?4],[Pair2Card4]) +!L([Pair3],[?2],[Pair3Card2]) +!L([Pair3],[?3],[Pair3Card3]) +([Waiting],[!pair1],[Pair1]) +([Waiting],[!pair2],[Pair2]) +([Waiting],[!pair3],[Pair3])