Develop

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.0-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

ialib/build.gradle

@@ -1,5 +1,5 @@
 plugins {
-    id 'org.jetbrains.kotlin.jvm' version '1.5.0'
+    id 'org.jetbrains.kotlin.jvm' version '1.6.0'
 }
 
 repositories {
@@ -9,17 +9,17 @@ repositories {
 dependencies {
     implementation 'org.jetbrains.kotlin:kotlin-stdlib'
     implementation 'log4j:log4j:1.2.17'
-    implementation 'com.google.guava:guava:30.1-jre'
-    implementation 'org.jgrapht:jgrapht-core:1.5.0'
-    implementation 'org.jetbrains.kotlinx:kotlinx-coroutines-core:1.5.0'
+    implementation 'com.google.guava:guava:31.0.1-jre'
+    implementation 'org.jgrapht:jgrapht-core:1.5.1'
+    implementation 'org.jetbrains.kotlinx:kotlinx-coroutines-core:1.6.0'
 }
 compileKotlin {
     kotlinOptions {
-        jvmTarget = "1.8"
+        jvmTarget = "11"
     }
 }
 compileTestKotlin {
     kotlinOptions {
-        jvmTarget = "1.8"
+        jvmTarget = "11"
     }
 }

run-assemble.sh

@@ -1,4 +1,6 @@
 #!/bin/bash
+export JAVA_HOME=`/usr/libexec/java_home -v 11`
+
 cd "$(dirname "$0")" || exit
 ./gradlew clean assemble || exit
 

run-test.sh

@@ -1,4 +1,6 @@
 #!/bin/bash
+export JAVA_HOME=`/usr/libexec/java_home -v 11`
+
 cd "$(dirname "$0")" || exit
 ./gradlew swtia:clean swtia:test || exit
 

samples/ey-examples/Example-Alternating.ia

@@ -0,0 +1,37 @@
+// Example to test the alternating simulation
+
+actions { a, b}
+var x : int
+
+proc ClientSpec {
+    act { a?, b? }
+
+    a?
+}
+
+proc ClientImpl {
+    act { a?, b? }
+
+    a?
+	b?
+}
+
+proc Server {
+	act { a!, b! }
+
+	a!
+	b!
+}
+
+init {
+    sys clientSpec = ClientSpec()
+    sys clientImpl = ClientImpl()
+    refinement(clientImpl, clientSpec)
+
+	sys server = Server()
+
+	sys compositionSpec = composition(server, clientSpec)
+	sys compositionImpl = composition(server, clientImpl)
+    refinement(compositionImpl, compositionSpec)
+
+}

samples/ey-examples/Example-ClientServer.ia

@@ -0,0 +1,42 @@
+actions { snd, ok, fail, trnsmt, ack, nack }
+var x: int
+
+proc Client1 {
+	act { snd!, ok?, fail? }
+	while {
+		x == 1 -> { snd! => ok? }
+		ok? -> {}
+	}
+}
+
+proc Client2 {
+    act { snd!, ok?, fail? }
+    loop {
+        case {
+            x > 0 -> snd!
+            x < 0 -> snd!
+	        ok? -> tau
+        }
+    }
+
+}
+
+proc Server {
+	act { snd?, trnsmt!, ack?, nack?, ok!, fail! }
+	while {
+		snd? -> {
+			trnsmt!
+			case {
+				ack? -> ok!
+				nack? -> fail!
+			}
+		}
+	}
+}
+
+init {
+	sys c1 = Client1()
+	refinement(Client1(), Client2())
+	sys prod = product(c1, Server())
+	sys comp = prune(prod)
+}

samples/ey-examples/Example-Demo.ia

@@ -0,0 +1,29 @@
+actions { coin, atVM }
+type Drink { Coffee, Tea }
+var drink : Drink
+var value : int
+
+proc MachineSpec {
+	act { coin? }
+	value < 2 => { coin? guarantee(value' >= value) }
+}
+
+proc MachineImpl {
+	act { coin? }
+	value < 3 => { coin? guarantee(value' > value) }
+}
+
+proc Customer {
+    act { atVM?, coin! }
+	drink == Coffee => atVM?
+	value < 2 => { coin! assume(value' > value) }
+}
+
+init {
+	sys machineSpec = MachineSpec()
+	sys customer = Customer()
+	sys comp = composition(machineSpec, customer)
+
+	sys machineImpl = MachineImpl()
+	refinement(machineImpl, machineSpec)
+}

samples/ey-examples/Example-EY1.ia

@@ -0,0 +1,34 @@
+// Example to test the generation of families during alternating simulation
+
+actions { a, b, c, d, e }
+var x : int
+
+proc Spec {
+    act { a?, b?, c!, d! }
+
+    x > 5 => a? guarantee(x' > 2*x)
+
+    case {
+        x >= 1 -> { c! assume(x' != 1) }
+        x == 0 -> { c! assume(x' == 1) }
+    }
+}
+
+proc Impl {
+    act { a?, b?, c!, d! }
+
+    case {
+        x == 5 -> { a? guarantee(x' > 2*x) }
+        x == 6 -> { a? guarantee(x' > 3*x) }
+        x >  6 -> { a? guarantee(x' > 4*x) }
+    }
+
+    x == 0 => { c! assume(x' > 0) }
+}
+
+init {
+    sys impl = Impl()
+    sys spec = Spec()
+
+    refinement(impl, spec)
+}

samples/ey-examples/Example-EY2.ia

@@ -0,0 +1,36 @@
+// Example to test the creation of a product automaton from a 
+// specification and from its implementation
+
+actions { b }
+var x : int
+
+proc P {
+	act { b! }
+
+	x > 0 => { b! assume(x' < 3) }
+}
+
+proc Q {
+	act { b! }
+
+	x > -2 => { b! assume(x' < 2) }
+}
+
+proc A {
+	act { b? }
+
+	x > -4 => { b? guarantee(x' < 0) }
+}
+
+init {
+	sys p = P()
+	sys q = Q()
+	sys a = A()
+
+	refinement(p, q)
+
+	sys pa = composition(p, a)
+	sys qa = composition(q, a)
+
+	refinement(pa, qa)
+}

samples/ey-examples/Example-EY3.ia

@@ -0,0 +1,23 @@
+actions {a, b}
+
+proc P {
+	act {a!}
+
+	true => a!
+}
+
+proc Q {
+	act {a?, b?}
+
+	true => b?
+	true => a?
+}
+
+init {
+	sys p = P()
+	sys q = Q()
+
+	refinement(p, q)
+
+	sys pq = composition(p, q)
+}

samples/ey-examples/Example-EY4.ia

@@ -0,0 +1,28 @@
+// Example to test the preservation of error states when 
+// computing a product
+
+actions { b }
+var x : int
+
+proc P {
+  act { b? }
+
+  b?
+}
+
+proc A {
+  act { b! }
+
+  case {
+    true -> { b! }
+    true -> { b! error }
+  }
+}
+
+init {
+  sys p = P()
+  sys a = A()
+
+  sys prod = product(p, a)
+  sys pruned = prune(prod)
+}

samples/ey-examples/Example-EY5.ia

@@ -0,0 +1,26 @@
+// Example to test the pruning of communication errors in
+// a product automaton
+
+actions { b }
+
+proc P {
+  act { b? }
+
+  b?
+}
+
+proc A {
+  act { b! }
+
+  case {
+    true -> { b! }
+    true -> { b! => b! }
+  }
+}
+
+init {
+  sys p = P()
+  sys a = A()
+
+  sys prod = product(p, a)
+}

samples/ey-examples/Example-Fig7.ia

@@ -0,0 +1,51 @@
+// Example in the Gareis2019 paper
+// Fig. 5 (page 13)
+
+actions { a, b }
+var x: int
+
+proc P {
+    act { a!, b? }
+    case {
+        x == 2 -> {
+            a!
+            assume(x' != 2)
+        }
+        x == -2 -> {
+            a!
+            assume(x' != -2)
+        }
+        true -> {
+            b?
+            case {
+                x >= 0 -> {
+                    a!
+                    assume(x' == 0)
+                }
+                x == 2 -> a!
+            }
+        }
+    }
+}
+
+proc Q {
+    act { a? }
+    case {
+        x > 0 -> {
+            a?
+            guarantee(x' < 0)
+        }
+        x < 0 -> {
+            a?
+            guarantee(x' > 0)
+        }
+    }
+}
+
+init {
+	sys p = P()
+	sys q = Q()
+
+    sys prod = product(p, q)
+    sys comp = prune(prod)
+}