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 <davide.basile@isti.cnr.it>

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<this.getRank();i++)
+			pr.append(Arrays.toString(
+					this.getBasicStates().get(i).stream()
+							.filter(BasicState::isCommitted)
+							.map(BasicState::getState)
+							.sorted()
+							.toArray()));
+		pr.append("]").append(System.lineSeparator());
 		pr.append("Transitions: ").append(System.lineSeparator());
 		this.getTransition().stream()
 				.sorted(Comparator.comparing(T::toString))
 				.forEach(t-> 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())));
+	}
 }

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 <code>Label</code>. <br>
  * The content of each label is a list of actions. <br>
  * Contract automata labels can be of three types:<br>
@@ -52,10 +53,11 @@ public CALabel(List<Action> 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<Action> 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()) {

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);
+    }
+}

src/main/java/io/github/contractautomata/catlib/automaton/state/AbstractState.java

@@ -18,6 +18,7 @@ public abstract class AbstractState<T> implements Ranked {
 	 */
 	private final T label;
 
+
 	/**
 	 * Constructs an abstract state from its label (content).
 	 * Label must be non-null

src/main/java/io/github/contractautomata/catlib/automaton/state/BasicState.java

@@ -22,6 +22,8 @@ public class BasicState<T> extends AbstractState<T>{
 	 */
 	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

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;
 	}
 
 	/**

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);

src/main/java/io/github/contractautomata/catlib/converters/AutDataConverter.java

@@ -73,6 +73,7 @@ public Automaton<String,Action,State<String>,ModalTransition<String,Action,State
 			int rank=0;
 			String[] initial = new String[1];
 			String[][] fin = new String[1][];
+			String[][] comm = new String[1][];
 			tr = new HashSet<>();
 			Set<State<String>> states = new HashSet<>();
 			Map<Integer,Set<BasicState<String>>> mapBasicStates = new HashMap<>();
@@ -97,17 +98,22 @@ public Automaton<String,Action,State<String>,ModalTransition<String,Action,State
 						}
 						case "F": //Final state
 						{
-							fin=readFinalState(strLine,rank);
+							fin= readCommittedOrFinalState(strLine,rank,"Final states");
+							break;
+						}
+						case "C": //Committed state
+						{
+							comm= readCommittedOrFinalState(strLine,rank,"Committed states");
 							break;
 						}
 						case "(": //a permitted transition
 						{
-							tr.add(loadTransition(strLine,rank, ModalTransition.Modality.PERMITTED, states,mapBasicStates,initial,fin));
+							tr.add(loadTransition(strLine,rank, ModalTransition.Modality.PERMITTED, states,mapBasicStates,initial,fin,comm));
 							break;
 						}
 						case ModalTransition.NECESSARY: //a necessary transition
 						{
-							tr.add(loadTransition(strLine,rank,readModality(strLine),states,mapBasicStates,initial,fin));
+							tr.add(loadTransition(strLine,rank,readModality(strLine),states,mapBasicStates,initial,fin,comm));
 							break;
 						}
 						default :
@@ -130,18 +136,18 @@ private String[] readInitialState(String strLine, int rank){
 		return initial;
 	}
 
-	private String[][] readFinalState(String strLine, int rank){
-		String[][] fin=Arrays.stream(strLine.split("]"))
+	private String[][] readCommittedOrFinalState(String strLine, int rank, String commOrFin){
+		String[][] states=Arrays.stream(strLine.split("]"))
 				.map(sar->Arrays.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<String,Action,State<String>,L> loadTransition(String str, int rank, ModalTransition.Modality type, Set<State<String>> states,Map<Integer,Set<BasicState<String>>> mapBasicStates,String[] initial, String[][] fin) throws IOException
+	private ModalTransition<String,Action,State<String>,L> loadTransition(String str, int rank, ModalTransition.Modality type, Set<State<String>> states,Map<Integer,Set<BasicState<String>>> mapBasicStates,String[] initial, String[][] fin, String[][] comm) throws IOException
 	{
 		String regex = "\\(\\["+"(.+)"+"\\],\\["+"(.+)"+"\\],\\["+"(.+)"+"\\]\\)";
 		Pattern pattern = Pattern.compile(regex);
@@ -172,8 +178,8 @@ private ModalTransition<String,Action,State<String>,L> loadTransition(String str
 				tr[2].length!=rank)
 			throw new IOException("Ill-formed transitions, different ranks");
 
-		State<String> source = createOrLoadState(states,mapBasicStates,tr[0],initial, fin);//source
-		State<String> target = createOrLoadState(states,mapBasicStates,tr[2],initial, fin);//target
+		State<String> source = createOrLoadState(states,mapBasicStates,tr[0],initial, fin, comm);//source
+		State<String> 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<String> createOrLoadState(Set<State<String>> states,Map<Integer,Set<BasicState<String>>> mapBasicStates, String[] state,String[] initial, String[][] fin)  {
+	private State<String> createOrLoadState(Set<State<String>> states,Map<Integer,Set<BasicState<String>>> 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<String> createOrLoadState(Set<State<String>> states,Map<Integer,Se
 										{
 											BasicState<String> 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])),
+													i<comm.length&&!Objects.isNull(comm[i])&& //for retrocompatibility
+															Arrays.stream(comm[i]).anyMatch(id->id.equals(state[i])));
 											if (l==null)
 												mapBasicStates.put(i, new HashSet<>(List.of(bs)));
 											else