From bd33cc07e056948d39ef257701918cc49d3b417e Mon Sep 17 00:00:00 2001
From: davidebasile <davide.basile@isti.cnr.it>
Date: Thu, 21 Dec 2023 17:45:31 +0100
Subject: [PATCH] fixed some errors

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>
---
 ...littingOrchestrationSynthesisOperator.java |  3 +++
 src/test/resources/Dealer.data                | 23 +++++++++++++++++++
 src/test/resources/Player.data                | 13 +++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 src/test/resources/Dealer.data
 create mode 100644 src/test/resources/Player.data

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<String,Action,State<String>,ModalTransition<String,Action,State
 		Automaton<String, Action, State<String>, ModalTransition<String, Action, State<String>, 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<String, Action, State<String>, ModalTransition<String, Action, State<String>, 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])