Add code examples showing the need for synchronization

examples/inputs/synchronization/Declassify-alice.txt

@@ -0,0 +1 @@
+42

examples/inputs/synchronization/Declassify-bob.txt

@@ -0,0 +1 @@
+43

examples/inputs/synchronization/PickANumber-alice.txt

@@ -0,0 +1 @@
+42

examples/inputs/synchronization/PickANumber-bob.txt

@@ -0,0 +1 @@
+41

examples/outputs/synchronization/Declassify-alice.txt

@@ -0,0 +1 @@
+false

examples/outputs/synchronization/PickANumber-alice.txt

@@ -0,0 +1 @@
+false

examples/outputs/synchronization/PickANumber-bob.txt

@@ -0,0 +1 @@
+false

examples/src/main/viaduct/synchronization/Declassify.via

@@ -0,0 +1,15 @@
+host alice : {A & B}
+host bob   : {B}
+
+fun main() {
+    let $pick = input int from alice;
+
+    let $guess = input int from bob;
+    let $trusted_guess = endorse $guess from {B};
+
+    let $revealed_pick@Replication(hosts = {alice, bob}) = declassify $pick to {A ⊓ B};
+    let $bob_wins = $revealed_pick == $trusted_guess;
+
+    output $bob_wins to alice;
+    /* output $bob_wins to bob; */
+}

examples/src/main/viaduct/synchronization/PickANumber.via

@@ -0,0 +1,16 @@
+host alice : {A}
+host bob   : {B & A<-}
+
+fun main() {
+    let $pick = input int from alice;
+    let $trusted_pick = endorse $pick from {A};
+
+    let $guess = input int from bob;
+    let $revealed_guess = declassify $guess to {A ⊓ B};
+
+    let $revealed_pick = declassify $trusted_pick to {A ⊓ B};
+    let $bob_wins = $revealed_pick == $revealed_guess;
+
+    output $bob_wins to alice;
+    output $bob_wins to bob;
+}

examples/src/test/kotlin/edu/cornell/cs/apl/viaduct/examples/RunExamplesTest.kt

@@ -12,6 +12,7 @@ import org.apache.logging.log4j.Level
 import org.apache.logging.log4j.core.config.Configurator
 import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.BeforeAll
+import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ArgumentsSource
 import org.springframework.util.SocketUtils
@@ -39,6 +40,22 @@ internal class RunExamplesTest {
         }
     }
 
+    /** Convenience function that creates empty input/output files for new test programs. */
+    @Disabled
+    @ParameterizedTest
+    @ArgumentsSource(ViaductProgramProvider::class)
+    fun createEmptyInputOutputFiles(program: ViaductGeneratedProgram) {
+        fun createFile(file: File) {
+            println("Creating $file.")
+            file.parentFile.mkdirs()
+            file.createNewFile()
+        }
+        program.hosts.forEach { host ->
+            createFile(inputFile(program, host))
+            createFile(outputFile(program, host))
+        }
+    }
+
     companion object {
         @BeforeAll
         @JvmStatic