New orchestration (#16)

* created new branch for implementing the new orchestration synthesis algorithm

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* implemented the NewOrchestrationSynthesisOperator.java class and test

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* fix

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* 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>

* fixed a typo in ModalTransition

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* fixed the constructor of BasicState.java to accept the committed flag.
fixed github actions script

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* update sonar.coverage.exclusions in pom.xml

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* trying to fix pom.xml for sonarcloud coverage

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* change name to SplittingOrchestrationSynthesisOperator.java

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* change name to SplittingOrchestrationSynthesisOperator.java

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* fixed some errors

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* update README (badges for the new branch) and pom.xml coveralls to ignore the unused src folder

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

* fixing a problem with sonarcloud running on ubuntu  with java 11

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

---------

Signed-off-by: Davide Basile <davide.basile@isti.cnr.it>

.github/workflows/build.yml

@@ -10,7 +10,7 @@ jobs:
   spot-bugs:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           # Disabling shallow clone is recommended for improving relevancy of reporting
           fetch-depth: 0
@@ -29,7 +29,7 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           # Disabling shallow clone is recommended for improving relevancy of reporting
           fetch-depth: 0
@@ -64,7 +64,7 @@ jobs:
         run: mvn coveralls:report --define repoToken=${{ secrets.COVERALLS_REPO_TOKEN }}
 
       - name: 🔎 SonarCloud Scan
-        if: ${{ matrix.os == 'ubuntu-latest' && matrix.java =='11'}}
+        if: ${{ matrix.os == 'ubuntu-latest' && matrix.java =='17'}}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}  # Needed to get PR information, if any
           SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
@@ -82,7 +82,7 @@ jobs:
       security-events: write
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           # Disabling shallow clone is recommended for improving relevancy of reporting
           fetch-depth: 0
@@ -103,21 +103,21 @@ jobs:
 
         # Initializes the CodeQL tools for scanning.
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@v1
+        uses: github/codeql-action/init@v2
 
       - name: Autobuild
-        uses: github/codeql-action/autobuild@v1
+        uses: github/codeql-action/autobuild@v2
 
       - name: 🔎 Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@v1
+        uses: github/codeql-action/analyze@v2
 
 
   mutationtesting: 
     needs: spot-bugs
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           # Disabling shallow clone is recommended for improving relevancy of reporting
           fetch-depth: 0

README.md

@@ -1,6 +1,6 @@
 ![Build and Testing](https://github.com/contractautomataproject/ContractAutomataLib/actions/workflows/build.yml/badge.svg)
-[![Coverage Status](https://coveralls.io/repos/github/ContractAutomataProject/ContractAutomataLib/badge.svg?branch=main)](https://coveralls.io/github/ContractAutomataProject/ContractAutomataLib?branch=main)
- [![Mutation testing badge](https://img.shields.io/endpoint?style=flat&url=https%3A%2F%2Fbadge-api.stryker-mutator.io%2Fgithub.com%2Fcontractautomataproject%2FContractAutomataLib%2Fmain)](https://dashboard.stryker-mutator.io/reports/github.com/contractautomataproject/ContractAutomataLib/main)
+[![Coverage Status](https://coveralls.io/repos/github/ContractAutomataProject/ContractAutomataLib/badge.svg?branch=newOrchestration)](https://coveralls.io/github/ContractAutomataProject/ContractAutomataLib?branch=newOrchestration)
+ [![Mutation testing badge](https://img.shields.io/endpoint?style=flat&url=https%3A%2F%2Fbadge-api.stryker-mutator.io%2Fgithub.com%2Fcontractautomataproject%2FContractAutomataLib%2FnewOrchestration)](https://dashboard.stryker-mutator.io/reports/github.com/contractautomataproject/ContractAutomataLib/newOrchestration)
 [![Quality Gate Status](https://sonarcloud.io/api/project_badges/measure?project=ContractAutomataProject_ContractAutomataLib&metric=alert_status)](https://sonarcloud.io/summary/new_code?id=ContractAutomataProject_ContractAutomataLib)
 [![Codacy Badge](https://app.codacy.com/project/badge/Grade/0f7dcd94be9141b1b64ef615edbb3991)](https://www.codacy.com/gh/contractautomataproject/ContractAutomataLib/dashboard?utm_source=github.com&utm_medium=referral&utm_content=contractautomataproject/ContractAutomataLib&utm_campaign=Badge_Grade)
 [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)

pom.xml

@@ -6,7 +6,7 @@
 	<!-- https://central.sonatype.org/publish/requirements/ -->
 	<groupId>io.github.contractautomataproject</groupId>
 	<artifactId>catlib</artifactId>
-	<version>1.0.2</version>
+	<version>1.0.3</version>
 	<packaging>jar</packaging>
 	<name>ContractAutomataLib</name>
 	<description>Library for specifying and verifying contract automata.</description>
@@ -56,6 +56,7 @@
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
 		<sonar.organization>contractautomataproject</sonar.organization>
 		<sonar.host.url>https://sonarcloud.io</sonar.host.url>
+		<sonar.coverage.exclusions>**/test/**/*.*,**/src/main/java/io/github/contractautomata/catlib/unused/*.*</sonar.coverage.exclusions>
 	</properties>
 	<dependencies>
 		<!-- https://mvnrepository.com/artifact/io.stryker-mutator/mutation-testing-elements -->
@@ -257,6 +258,9 @@
 						<jacocoReports>
 							<jacocoReport>${project.reporting.outputDirectory}/jacoco/jacoco.xml</jacocoReport>
 						</jacocoReports>
+						<excludes>
+							<exclude>src/main/java/io/github/contractautomata/catlib/unused</exclude>
+						</excludes>
 					</configuration>
 					<dependencies>
 						<!-- https://mvnrepository.com/artifact/javax.xml.bind/jaxb-api -->
@@ -275,6 +279,7 @@
 					<configuration>
 						<excludes>
 							<exclude>test/*</exclude>
+							<exclude>src/main/java/io/github/contractautomata/catlib/unused</exclude>
 						</excludes>
 					</configuration>
 					<executions>

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,21 @@ 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 +160,7 @@ public boolean isMatch()
 	 */
 	public boolean isOffer()
 	{
-		return getRequesterIfAny() == -1;
+		return !this.isTau() &&  getRequesterIfAny() == -1;
 	}
 
 
@@ -139,7 +170,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 +205,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 +235,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,12 @@ public class BasicState<T> extends AbstractState<T>{
 	 */
 	private final boolean fin;
 
+	/**
+	 * the flag signalling if the state is committed
+	 */
+	private final boolean committed;
+
+
 	/**
 	 * Constructor for a BasicState.
 	 * Label must not be a list of elements, and elements
@@ -31,13 +37,17 @@ public class BasicState<T> extends AbstractState<T>{
 	 * @param label the content of the state
 	 * @param init  true if it is initial
 	 * @param fin true if it is final
+	 * @param committed true if the state is committed
 	 */
-	public BasicState(T label, Boolean init, Boolean fin) {
+	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 +78,8 @@ public boolean isInitial() {
 		return init;
 	}
 
+	public boolean isCommitted() {return committed;}
+
 
 	/**
 	 * Print a String representing this object