From d2c023dd110aa918c94cbcbe16102f5ce4d106db Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Fri, 31 Mar 2023 18:26:56 +0200
Subject: [PATCH 01/20] trying to add methods to thread classes

---
 src/main/vct/main/stages/Transformation.scala |  4 +-
 .../veymont/ParalleliseVeyMontThreads.scala   | 85 +++++++++++++++++++
 2 files changed, 88 insertions(+), 1 deletion(-)
 create mode 100644 src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala

diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index 402360dcd7..fabab8fab9 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -25,6 +25,7 @@ import vct.options.Options
 import vct.parsers.transform.BlameProvider
 import vct.resources.Resources
 import vct.result.VerificationError.SystemError
+import vct.rewrite.veymont.ParalleliseVeyMontThreads
 
 object Transformation {
   case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[CheckError]) extends SystemError {
@@ -293,6 +294,7 @@ case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Veri
   extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
-    StructureCheck
+    StructureCheck,
+    ParalleliseVeyMontThreads
   ))
 
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
new file mode 100644
index 0000000000..711f9e38d2
--- /dev/null
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -0,0 +1,85 @@
+package vct.rewrite.veymont
+
+import hre.util.ScopedStack
+import vct.col.ast.{BooleanValue, Class, ClassDeclaration, Declaration, InstanceField, InstanceMethod, Node, Program, VeyMontSeqProg, VeyMontThread}
+import vct.col.origin.{Origin, PreferredNameOrigin}
+import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+import vct.col.typerules.CoercionUtils.o
+import vct.result.VerificationError.UserError
+import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ParalliseVeyMontThreadsError, ThreadClassOrigin}
+
+object ParalleliseVeyMontThreads extends RewriterBuilder {
+  override def key: String = "ParalleliseVeyMontThreads"
+
+  override def desc: String = "Generate classes for VeyMont threads in parallel program"
+
+  case class ParalliseVeyMontThreadsError(node : Node[_], msg: String) extends UserError {
+    override def code: String = "ParalleliseVeyMontThreadsError"
+
+    override def text: String = node.o.messageInContext(msg)
+  }
+
+  case class ThreadClassOrigin(thread: VeyMontThread[_]) extends Origin {
+    override def preferredName: String = thread.o.preferredName.toUpperCase() + "Thread"
+
+    override def context: String = thread.o.context
+
+    override def inlineContext: String = thread.o.inlineContext
+
+    override def shortPosition: String = thread.o.shortPosition
+  }
+}
+
+case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre] {
+
+  val inSeqProg: ScopedStack[VeyMontThread[Pre]] = ScopedStack()
+
+
+  override def dispatch(decl : Declaration[Pre]) : Unit = {
+    decl match {
+      case seqProg: VeyMontSeqProg[Pre] =>
+        val threadClasses = generateThreadClasses(seqProg)
+        for(tc <- threadClasses) {
+          globalDeclarations.declare(tc)
+        }
+      case other => rewriteDefault(other)
+    }
+  }
+
+
+  private def generateThreadClasses(seqProg: VeyMontSeqProg[Pre]) : Seq[Class[Post]] = {
+    val threadClasses = seqProg.threads.map { t =>
+      inSeqProg.push(t)
+      try {
+        classDeclarations.scope {
+          val threadField = new InstanceField[Post](dispatch(t.threadType), Set.empty)(t.o)
+          val methods: Seq[ClassDeclaration[Post]] = seqProg.methods.map {
+            case m: InstanceMethod[Pre] => getThreadMethod(t, m)
+            case _ => throw ParalliseVeyMontThreadsError(seqProg, "Methods of seq_program need to be of type InstanceMethod")
+          }
+          new Class[Post](
+            threadField +: methods,
+            Seq(),
+            BooleanValue(true)(t.o))(ThreadClassOrigin(t))
+        }
+      } finally {
+        inSeqProg.pop()
+      }
+    }
+    threadClasses
+  }
+
+
+  private def getThreadMethod(thread: VeyMontThread[Pre], method : InstanceMethod[Pre]): InstanceMethod[Post] = {
+    new InstanceMethod[Post](
+        dispatch(method.returnType),
+        variables.dispatch(method.args),
+        variables.dispatch(method.outArgs),
+        variables.dispatch(method.typeArgs),
+        method.body.map(dispatch),
+        dispatch(method.contract))(method.blame)(method.o)
+  }
+
+
+}

From 63b5ed684215ed4aae516c57b32bd0da5fccedc9 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Mon, 3 Apr 2023 17:19:17 +0200
Subject: [PATCH 02/20] partial code for adding channel fields

---
 .../veymont-seq-progs/veymont-swap.pvl        |  2 +-
 .../veymont/ParalleliseVeyMontThreads.scala   | 82 +++++++++++++++----
 .../vct/rewrite/veymont/StructureCheck.scala  |  8 ++
 3 files changed, 76 insertions(+), 16 deletions(-)

diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/examples/technical/veymont-seq-progs/veymont-swap.pvl
index 72e1c70988..a4d40454c8 100644
--- a/examples/technical/veymont-seq-progs/veymont-swap.pvl
+++ b/examples/technical/veymont-seq-progs/veymont-swap.pvl
@@ -28,7 +28,7 @@ seq_program SeqProgram(int x, int y) {
      s1.temp = 5;
   }
   
-  void bar(int a) {}
+  //void bar(int a) {}
 
   run {
     if(s1.v == 5 && s2.v == 6) {
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 711f9e38d2..71d50038f5 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,14 +1,17 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.{BooleanValue, Class, ClassDeclaration, Declaration, InstanceField, InstanceMethod, Node, Program, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Eval, InstanceField, InstanceMethod, Loop, Node, Program, RunMethod, Scope, Statement, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
+import vct.col.ref.Ref
 import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
 import vct.col.typerules.CoercionUtils.o
 import vct.result.VerificationError.UserError
 import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ParalliseVeyMontThreadsError, ThreadClassOrigin}
 
+import scala.collection.immutable.Map
+
 object ParalleliseVeyMontThreads extends RewriterBuilder {
   override def key: String = "ParalleliseVeyMontThreads"
 
@@ -34,44 +37,48 @@ object ParalleliseVeyMontThreads extends RewriterBuilder {
 case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre] {
 
   val inSeqProg: ScopedStack[VeyMontThread[Pre]] = ScopedStack()
-
+  val inSeqThreadMap : ScopedStack[Map[VeyMontThread[Pre],InstanceField[Post]]] = ScopedStack()
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
-        val threadClasses = generateThreadClasses(seqProg)
-        for(tc <- threadClasses) {
-          globalDeclarations.declare(tc)
+        val threadFieldMap = generateThreadFields(seqProg)
+        inSeqThreadMap.having(threadFieldMap) {
+          val threadClasses = generateThreadClasses(seqProg)
+          for (tc <- threadClasses) {
+            globalDeclarations.declare(tc)
+          }
         }
+      case t: VeyMontThread[Pre] => //sucessor is threadField in threadClass constructed above
       case other => rewriteDefault(other)
     }
   }
 
+  private def generateThreadFields(seqProg: VeyMontSeqProg[Pre]) : Map[VeyMontThread[Pre],InstanceField[Post]] =
+    seqProg.threads.map { thread => (thread -> new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)) }.toMap
 
   private def generateThreadClasses(seqProg: VeyMontSeqProg[Pre]) : Seq[Class[Post]] = {
-    val threadClasses = seqProg.threads.map { t =>
-      inSeqProg.push(t)
-      try {
+    val threadClasses = seqProg.threads.map { thread =>
+      inSeqProg.having(thread) {
+        val threadFieldMap = inSeqThreadMap.top
         classDeclarations.scope {
-          val threadField = new InstanceField[Post](dispatch(t.threadType), Set.empty)(t.o)
+          val channelFields = getChannelFields(collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg))
           val methods: Seq[ClassDeclaration[Post]] = seqProg.methods.map {
-            case m: InstanceMethod[Pre] => getThreadMethod(t, m)
+            case m: InstanceMethod[Pre] => getThreadMethod(m)
             case _ => throw ParalliseVeyMontThreadsError(seqProg, "Methods of seq_program need to be of type InstanceMethod")
           }
           new Class[Post](
-            threadField +: methods,
+            (threadFieldMap(thread) +: channelFields) ++ methods,
             Seq(),
-            BooleanValue(true)(t.o))(ThreadClassOrigin(t))
+            BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
         }
-      } finally {
-        inSeqProg.pop()
       }
     }
     threadClasses
   }
 
 
-  private def getThreadMethod(thread: VeyMontThread[Pre], method : InstanceMethod[Pre]): InstanceMethod[Post] = {
+  private def getThreadMethod(method : InstanceMethod[Pre]): InstanceMethod[Post] = {
     new InstanceMethod[Post](
         dispatch(method.returnType),
         variables.dispatch(method.args),
@@ -81,5 +88,50 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
         dispatch(method.contract))(method.blame)(method.o)
   }
 
+  private def getChannelFields(chanDescr : Seq[(Type[Pre], String,Statement[Pre])]): Seq[InstanceField[Post]] = Seq.empty
+  //InstanceField[Post](dispatch(ChannelClassOfRightType), Set.empty)(ChannelOrigin)
+
+  private def collectChannelsFromRun(seqProg : VeyMontSeqProg[Pre]) =
+    seqProg.runMethod match {
+      case r: RunMethod[Pre] => getChannelsFromBody(r.body, r)
+      case other => throw ParalliseVeyMontThreadsError(other, "seq_program run method expected")
+    }
+
+  private def collectChannelsFromMethods(seqProg: VeyMontSeqProg[Pre]) =
+    seqProg.methods.flatMap {
+    case m: InstanceMethod[Pre] => getChannelsFromBody(m.body, m)
+    case other => throw ParalliseVeyMontThreadsError(other, "seq_program method expected")
+  }
 
+  private def getChannelsFromBody(body: Option[Statement[Pre]], method: ClassDeclaration[Pre]) = {
+    body match {
+      case None => throw ParalliseVeyMontThreadsError(method, "Method in seq_program needs to have non-empty body")
+      case Some(b) => getChannelNamesAndTypes(b)
+    }
+  }
+
+  private def getChannelNamesAndTypes(s : Statement[Pre]): Seq[(Type[Pre], String,Statement[Pre])] = {
+    s.collect{case e@VeyMontCommExpression(recv,sender,assign) =>
+      (recv.decl.threadType,recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel",e)}
+  }
+/*
+  override def dispatch(st : Statement[Pre]) : Statement[Post] = {
+    if (inSeqProg.nonEmpty) {
+      val thread = inSeqProg.top
+      val threadFieldMap = inSeqThreadMap.top
+      st match {
+        case VeyMontCommExpression(recv,sender,assign) => dispatch(assign)
+        case VeyMontAssignExpression(_, _) => rewriteDefault(st)
+        case Assign(_, _) => rewriteDefault(st)
+        case Branch(_) => rewriteDefault(st)
+        case Loop(_, _, _, _, _) => rewriteDefault(st)
+        case Scope(_, _) => rewriteDefault(st)
+        case Block(_) => rewriteDefault(st)
+        case Eval(expr) => dispatch(expr)
+        case Assert(_) => rewriteDefault(st)
+        case _ => throw VeyMontStructCheckError(st, "Statement not allowed in seq_program")
+      }
+    } else rewriteDefault(st)
+  }
+*/
 }
diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
index 897517f779..3ec673277d 100644
--- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
+++ b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
@@ -30,6 +30,14 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
       case dcl: VeyMontSeqProg[Pre] => inSeqProg.having(()) {
         rewriteDefault(dcl)
       }
+      case m: InstanceMethod[Pre] =>
+        if (inSeqProg.nonEmpty && m.args.nonEmpty)
+          throw VeyMontStructCheckError(m, "Methods in seq_program cannot have any arguments!")
+        else rewriteDefault(decl)
+      case r: RunMethod[Pre] =>
+        if(r.body.isEmpty)
+          throw VeyMontStructCheckError(r, "Method run in seq_program needs to have a body!")
+        else rewriteDefault(decl)
       case _ => rewriteDefault(decl)
     }
 

From 5353014bddb660dcfad0e80de5bbe22fbe5d1380 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 4 Apr 2023 17:12:17 +0200
Subject: [PATCH 03/20] importing Channel class

---
 res/universal/res/include/IntegerChannel.java | 12 +++++-------
 src/main/vct/importer/Util.scala              | 19 +++++++++++++++++--
 src/main/vct/main/stages/Transformation.scala | 13 ++++++++-----
 src/main/vct/options/Options.scala            |  2 ++
 src/main/vct/resources/Resources.scala        |  1 +
 5 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/res/universal/res/include/IntegerChannel.java b/res/universal/res/include/IntegerChannel.java
index cabccaf06a..18d125e501 100644
--- a/res/universal/res/include/IntegerChannel.java
+++ b/res/universal/res/include/IntegerChannel.java
@@ -1,16 +1,14 @@
-package include;
-
-public final class IntegerChannel {
+public final class Channel {
 
     private boolean transfering;
 
-    private int exchangeValue;
+    private MessageType exchangeValue;
 
-    public IntegerChannel() {
+    public Channel() {
         transfering = true;
     }
 
-    public synchronized void writeValue(int v) {
+    public synchronized void writeValue(MessageType v) {
         while (!transfering) {
             try {
                 wait();
@@ -23,7 +21,7 @@ public synchronized void writeValue(int v) {
         notify();
     }
 
-    public synchronized int readValue() {
+    public synchronized MessageType readValue() {
         while (transfering) {
             try {
                 wait();
diff --git a/src/main/vct/importer/Util.scala b/src/main/vct/importer/Util.scala
index ab582c2fd0..780eadd871 100644
--- a/src/main/vct/importer/Util.scala
+++ b/src/main/vct/importer/Util.scala
@@ -1,11 +1,11 @@
 package vct.importer
 
 import hre.io.Readable
-import vct.col.ast.Program
+import vct.col.ast.{JavaClass, JavaNamespace, Program}
 import vct.col.origin.{Blame, VerificationFailure}
 import vct.col.rewrite.Disambiguate
 import vct.main.stages.Resolution
-import vct.parsers.ColPVLParser
+import vct.parsers.{ColJavaParser, ColPVLParser}
 import vct.parsers.transform.{ConstantBlameProvider, ReadableOriginProvider}
 import vct.result.VerificationError.UserError
 
@@ -27,4 +27,19 @@ case object Util {
     val unambiguousProgram: Program[_] = Disambiguate().dispatch(context.tasks.head.program)
     unambiguousProgram.asInstanceOf[Program[G]]
   }
+
+  case class JavaLoadError(error: String) extends UserError {
+    override def code: String = "JavaClassLoadError"
+
+    override def text: String = error
+  }
+
+  def loadJavaClass[G](readable: Readable): JavaClass[G] =
+    ColJavaParser(ReadableOriginProvider(readable), ConstantBlameProvider(LibraryFileBlame)).parse(readable).decls match {
+      case Seq(javaNamespace: JavaNamespace[G]) => javaNamespace.declarations match {
+        case Seq(javaClass: JavaClass[G]) => javaClass
+        case seq => throw JavaLoadError("Expected to load exactly one Java class but found " + seq.size)
+      }
+      case seq => throw JavaLoadError("Expected to load exactly one Java name space but found " + seq.size)
+    }
 }
diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index fabab8fab9..f45e23c8a6 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -4,7 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.debug.TimeTravel
 import hre.progress.Progress
 import hre.stages.Stage
-import vct.col.ast.{Deserialize, IterationContract, Procedure, Program, RunMethod, Serialize, SimplificationRule, Verification, VerificationContext}
+import vct.col.ast.{Deserialize, IterationContract, JavaClass, Procedure, Program, RunMethod, Serialize, SimplificationRule, Verification, VerificationContext}
 import vct.col.check.CheckError
 import vct.col.feature
 import vct.col.feature.Feature
@@ -25,7 +25,7 @@ import vct.options.Options
 import vct.parsers.transform.BlameProvider
 import vct.resources.Resources
 import vct.result.VerificationError.SystemError
-import vct.rewrite.veymont.ParalleliseVeyMontThreads
+import vct.rewrite.veymont.{ChannelClassGenerator, ParalleliseVeyMontThreads}
 
 object Transformation {
   case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[CheckError]) extends SystemError {
@@ -73,7 +73,8 @@ object Transformation {
       case Backend.Silicon | Backend.Carbon =>
         VeyMontTransformation(
           onBeforePassKey = writeOutFunctions(options.outputBeforePass),
-          onAfterPassKey = writeOutFunctions(options.outputAfterPass)
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass),
+          channelClass = Util.loadJavaClass(options.veymontChannel),
         )
     }
 }
@@ -290,11 +291,13 @@ case class SilverTransformation
   ))
 
 case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
-                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil)
+                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                                 val channelClass: JavaClass[_])
   extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
     StructureCheck,
-    ParalleliseVeyMontThreads
+    ParalleliseVeyMontThreads,
+    ChannelClassGenerator.withArg(channelClass)
   ))
 
diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala
index c13812c03c..2f34e41df0 100644
--- a/src/main/vct/options/Options.scala
+++ b/src/main/vct/options/Options.scala
@@ -6,6 +6,7 @@ import vct.main.BuildInfo
 import vct.main.stages.Parsing.Language
 import vct.options.types.{Backend, ClassPathEntry, Mode, PathOrStd, ReadLanguage, Verbosity}
 import vct.resources.Resources
+import vct.resources.Resources.getVeymontChannel
 
 import java.nio.file.{Path, Paths}
 import scala.collection.mutable
@@ -379,6 +380,7 @@ case class Options
 
   // VeyMont options
   veymontOutput: PathOrStd = null, // required
+  veymontChannel: PathOrStd = PathOrStd.Path(getVeymontChannel),
 
   // VeSUV options
   vesuvOutput: PathOrStd = null,
diff --git a/src/main/vct/resources/Resources.scala b/src/main/vct/resources/Resources.scala
index 9507218be9..3ac0480d5e 100644
--- a/src/main/vct/resources/Resources.scala
+++ b/src/main/vct/resources/Resources.scala
@@ -17,4 +17,5 @@ case object Resources {
   def getJrePath: Path = getResource("/jdk")
   def getCcPath: Path = Paths.get("clang")
   def getSystemCConfig: Path = getResource("/systemc/config")
+  def getVeymontChannel: Path = getResource("/include/IntegerChannel.java")
 }

From 1499e9363f2b042fd156fe01d7437a22b7135f88 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Wed, 31 May 2023 17:10:42 +0200
Subject: [PATCH 04/20] rewriting channel classes gives NoSuchElementException

---
 src/main/vct/main/stages/Transformation.scala |  3 +-
 .../veymont/ChannelClassGenerator.scala       | 21 +++++
 .../veymont/ParalleliseVeyMontThreads.scala   | 88 ++++++++++++-------
 3 files changed, 79 insertions(+), 33 deletions(-)
 create mode 100644 src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala

diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index f45e23c8a6..be200d3c06 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -297,7 +297,6 @@ case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Veri
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
     StructureCheck,
-    ParalleliseVeyMontThreads,
-    ChannelClassGenerator.withArg(channelClass)
+    ParalleliseVeyMontThreads.withArg(channelClass),
   ))
 
diff --git a/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala b/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala
new file mode 100644
index 0000000000..71f26d53d4
--- /dev/null
+++ b/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala
@@ -0,0 +1,21 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.Type
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
+
+object ChannelClassGenerator extends RewriterBuilderArg[Type[_]] {
+  override def key: String = "ChannelClassGenerator"
+
+  override def desc: String = "Generate classes for channels of a VeyMont seq_program"
+
+}
+
+case class ChannelClassGenerator [Pre <: Generation](channelType: Type[_]) extends Rewriter[Pre] {
+
+  override def dispatch(t: Type[Pre]) : Type[Post] = {
+    if(t.o.preferredName == "MessageType")
+      dispatch(channelType.asInstanceOf[Type[Pre]])
+    else rewriteDefault(t)
+  }
+
+}
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 71d50038f5..7fc3575136 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,18 +1,14 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Eval, InstanceField, InstanceMethod, Loop, Node, Program, RunMethod, Scope, Statement, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.RewriteHelpers.RewriteJavaClass
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Eval, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, Node, Program, RunMethod, Scope, Statement, TClass, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
-import vct.col.ref.Ref
-import vct.col.rewrite.veymont.StructureCheck.VeyMontStructCheckError
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
-import vct.col.typerules.CoercionUtils.o
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
 import vct.result.VerificationError.UserError
-import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ParalliseVeyMontThreadsError, ThreadClassOrigin}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelClassOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
 
-import scala.collection.immutable.Map
-
-object ParalleliseVeyMontThreads extends RewriterBuilder {
+object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   override def key: String = "ParalleliseVeyMontThreads"
 
   override def desc: String = "Generate classes for VeyMont threads in parallel program"
@@ -32,9 +28,19 @@ object ParalleliseVeyMontThreads extends RewriterBuilder {
 
     override def shortPosition: String = thread.o.shortPosition
   }
+
+  case class ChannelClassOrigin(channelName: String, assign: Statement[_]) extends Origin {
+    override def preferredName: String = channelName
+
+    override def context: String = assign.o.context
+
+    override def inlineContext: String = assign.o.inlineContext
+
+    override def shortPosition: String = assign.o.shortPosition
+  }
 }
 
-case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre] {
+case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] {
 
   val inSeqProg: ScopedStack[VeyMontThread[Pre]] = ScopedStack()
   val inSeqThreadMap : ScopedStack[Map[VeyMontThread[Pre],InstanceField[Post]]] = ScopedStack()
@@ -43,8 +49,14 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
         val threadFieldMap = generateThreadFields(seqProg)
+        val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
+        val channelClasses = generateChannelClasses(channelInfo)
+        for (cc <- channelClasses.values) {
+          globalDeclarations.declare(cc)
+        }
+        val channelFields = getChannelFields(channelInfo, channelClasses)
         inSeqThreadMap.having(threadFieldMap) {
-          val threadClasses = generateThreadClasses(seqProg)
+          val threadClasses = generateThreadClasses(seqProg, channelFields)
           for (tc <- threadClasses) {
             globalDeclarations.declare(tc)
           }
@@ -57,12 +69,11 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
   private def generateThreadFields(seqProg: VeyMontSeqProg[Pre]) : Map[VeyMontThread[Pre],InstanceField[Post]] =
     seqProg.threads.map { thread => (thread -> new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)) }.toMap
 
-  private def generateThreadClasses(seqProg: VeyMontSeqProg[Pre]) : Seq[Class[Post]] = {
+  private def generateThreadClasses(seqProg: VeyMontSeqProg[Pre], channelFields: Seq[InstanceField[Post]]) : Seq[Class[Post]] = {
     val threadClasses = seqProg.threads.map { thread =>
       inSeqProg.having(thread) {
         val threadFieldMap = inSeqThreadMap.top
         classDeclarations.scope {
-          val channelFields = getChannelFields(collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg))
           val methods: Seq[ClassDeclaration[Post]] = seqProg.methods.map {
             case m: InstanceMethod[Pre] => getThreadMethod(m)
             case _ => throw ParalliseVeyMontThreadsError(seqProg, "Methods of seq_program need to be of type InstanceMethod")
@@ -77,21 +88,24 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
     threadClasses
   }
 
-
-  private def getThreadMethod(method : InstanceMethod[Pre]): InstanceMethod[Post] = {
-    new InstanceMethod[Post](
-        dispatch(method.returnType),
-        variables.dispatch(method.args),
-        variables.dispatch(method.outArgs),
-        variables.dispatch(method.typeArgs),
-        method.body.map(dispatch),
-        dispatch(method.contract))(method.blame)(method.o)
+  private def getChannelFields(channelInfo: Seq[(Type[Pre], String, Statement[Pre])], channelClasses: Map[Type[Pre],JavaClass[Post]]): Seq[InstanceField[Post]] = {
+    channelInfo.map { case (chanType, chanName, assign) =>
+      new InstanceField[Post](JavaTClass(channelClasses(chanType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanName,assign)) }
   }
 
-  private def getChannelFields(chanDescr : Seq[(Type[Pre], String,Statement[Pre])]): Seq[InstanceField[Post]] = Seq.empty
-  //InstanceField[Post](dispatch(ChannelClassOfRightType), Set.empty)(ChannelOrigin)
+  private def generateChannelClasses(channelInfo: Seq[(Type[Pre], String, Statement[Pre])]) : Map[Type[Pre],JavaClass[Post]] = {
+    val channelTypes = channelInfo.map(_._1).toSet
+    channelTypes.map(channelType =>
+      channelType -> {
+        val chanClassPre = channelClass.asInstanceOf[JavaClass[Pre]]
+        new RewriteJavaClass[Pre, Post](chanClassPre)(new ChannelClassGenerator[Pre](channelType)).rewrite(decls = classDeclarations.collect {
+          chanClassPre.decls.foreach(d => dispatch(d))
+        }._1)
+      }
+    ).toMap
+  }//new ChannelClassGenerator(channelType).globalDeclarations.dispatch(channelClass.unsafeTransmuteGeneration[JavaClass, Pre])
 
-  private def collectChannelsFromRun(seqProg : VeyMontSeqProg[Pre]) =
+  private def collectChannelsFromRun(seqProg: VeyMontSeqProg[Pre]) =
     seqProg.runMethod match {
       case r: RunMethod[Pre] => getChannelsFromBody(r.body, r)
       case other => throw ParalliseVeyMontThreadsError(other, "seq_program run method expected")
@@ -99,9 +113,9 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
 
   private def collectChannelsFromMethods(seqProg: VeyMontSeqProg[Pre]) =
     seqProg.methods.flatMap {
-    case m: InstanceMethod[Pre] => getChannelsFromBody(m.body, m)
-    case other => throw ParalliseVeyMontThreadsError(other, "seq_program method expected")
-  }
+      case m: InstanceMethod[Pre] => getChannelsFromBody(m.body, m)
+      case other => throw ParalliseVeyMontThreadsError(other, "seq_program method expected")
+    }
 
   private def getChannelsFromBody(body: Option[Statement[Pre]], method: ClassDeclaration[Pre]) = {
     body match {
@@ -110,10 +124,22 @@ case class ParalleliseVeyMontThreads[Pre <: Generation]() extends Rewriter[Pre]
     }
   }
 
-  private def getChannelNamesAndTypes(s : Statement[Pre]): Seq[(Type[Pre], String,Statement[Pre])] = {
-    s.collect{case e@VeyMontCommExpression(recv,sender,assign) =>
-      (recv.decl.threadType,recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel",e)}
+  private def getChannelNamesAndTypes(s: Statement[Pre]): Seq[(Type[Pre], String, Statement[Pre])] = {
+    s.collect { case e@VeyMontCommExpression(recv, sender, assign) =>
+      (recv.decl.threadType, recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel", e)
+    }
   }
+
+  private def getThreadMethod(method : InstanceMethod[Pre]): InstanceMethod[Post] = {
+    new InstanceMethod[Post](
+        dispatch(method.returnType),
+        variables.dispatch(method.args),
+        variables.dispatch(method.outArgs),
+        variables.dispatch(method.typeArgs),
+        method.body.map(dispatch),
+        dispatch(method.contract))(method.blame)(method.o)
+  }
+
 /*
   override def dispatch(st : Statement[Pre]) : Statement[Post] = {
     if (inSeqProg.nonEmpty) {

From 7f20f3f73e32f67b426714a3d5395e0e2edc1a28 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Wed, 31 May 2023 17:29:09 +0200
Subject: [PATCH 05/20] NoSuchElementException resolved

---
 .../vct/rewrite/veymont/ParalleliseVeyMontThreads.scala        | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 7fc3575136..5b3f3b1aae 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -51,9 +51,6 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         val threadFieldMap = generateThreadFields(seqProg)
         val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
         val channelClasses = generateChannelClasses(channelInfo)
-        for (cc <- channelClasses.values) {
-          globalDeclarations.declare(cc)
-        }
         val channelFields = getChannelFields(channelInfo, channelClasses)
         inSeqThreadMap.having(threadFieldMap) {
           val threadClasses = generateThreadClasses(seqProg, channelFields)

From c67dc4ca6ca7a370b56406eee9ac13b4cc759af8 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Thu, 1 Jun 2023 12:29:58 +0200
Subject: [PATCH 06/20] running without errors but no thread classes printed

---
 .../vct/rewrite/veymont/ChannelInfo.scala     |  8 ++
 .../veymont/ParalleliseVeyMontThreads.scala   | 84 +++++++++++--------
 .../veymont/ThreadBuildingBlocks.scala        |  9 ++
 3 files changed, 67 insertions(+), 34 deletions(-)
 create mode 100644 src/rewrite/vct/rewrite/veymont/ChannelInfo.scala
 create mode 100644 src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala

diff --git a/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala b/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala
new file mode 100644
index 0000000000..294b180630
--- /dev/null
+++ b/src/rewrite/vct/rewrite/veymont/ChannelInfo.scala
@@ -0,0 +1,8 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.{Type, VeyMontCommExpression}
+import vct.col.rewrite.Generation
+
+class ChannelInfo[Pre <: Generation](val comExpr: VeyMontCommExpression[Pre], val channelType: Type[Pre], val channelName: String) {
+
+}
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 5b3f3b1aae..422e9a0f55 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -4,6 +4,7 @@ import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.RewriteJavaClass
 import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Eval, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, Node, Program, RunMethod, Scope, Statement, TClass, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
+import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
 import vct.result.VerificationError.UserError
 import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelClassOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
@@ -43,55 +44,64 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
 case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] {
 
   val inSeqProg: ScopedStack[VeyMontThread[Pre]] = ScopedStack()
-  val inSeqThreadMap : ScopedStack[Map[VeyMontThread[Pre],InstanceField[Post]]] = ScopedStack()
+  val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
-        val threadFieldMap = generateThreadFields(seqProg)
         val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
         val channelClasses = generateChannelClasses(channelInfo)
         val channelFields = getChannelFields(channelInfo, channelClasses)
-        inSeqThreadMap.having(threadFieldMap) {
-          val threadClasses = generateThreadClasses(seqProg, channelFields)
-          for (tc <- threadClasses) {
-            globalDeclarations.declare(tc)
-          }
+        threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods,channelFields)) {
+          seqProg.threads.foreach(t =>
+            inSeqProg.having(t) {
+              dispatch(t)
+            })
         }
-      case t: VeyMontThread[Pre] => //sucessor is threadField in threadClass constructed above
+      case thread: VeyMontThread[Pre] => {
+        if(threadBuildingBlocks.nonEmpty) {
+          val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+          val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
+          val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
+            _.decl == thread
+          }.values.toSeq
+          val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
+          val threadMethods: Seq[ClassDeclaration[Post]] = threadRes.methods.map(getThreadMethodFromDecl(thread))
+          classDeclarations.scope {
+            //classDeclarations.collect {
+            val threadClass = new Class[Post](
+              (threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods),
+              Seq(),
+              BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
+            //globalDeclarations.declare(threadClass)
+          }
+        } else rewriteDefault(thread)
+      }
       case other => rewriteDefault(other)
     }
   }
 
-  private def generateThreadFields(seqProg: VeyMontSeqProg[Pre]) : Map[VeyMontThread[Pre],InstanceField[Post]] =
-    seqProg.threads.map { thread => (thread -> new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)) }.toMap
+  private def getThreadMethodFromDecl(thread: VeyMontThread[Pre])(decl: ClassDeclaration[Pre]): InstanceMethod[Post]  = decl match {
+    case m: InstanceMethod[Pre] => getThreadMethod(m)
+    case _ => throw ParalliseVeyMontThreadsError(thread, "Methods of seq_program need to be of type InstanceMethod")
+  }
 
-  private def generateThreadClasses(seqProg: VeyMontSeqProg[Pre], channelFields: Seq[InstanceField[Post]]) : Seq[Class[Post]] = {
-    val threadClasses = seqProg.threads.map { thread =>
-      inSeqProg.having(thread) {
-        val threadFieldMap = inSeqThreadMap.top
-        classDeclarations.scope {
-          val methods: Seq[ClassDeclaration[Post]] = seqProg.methods.map {
-            case m: InstanceMethod[Pre] => getThreadMethod(m)
-            case _ => throw ParalliseVeyMontThreadsError(seqProg, "Methods of seq_program need to be of type InstanceMethod")
-          }
-          new Class[Post](
-            (threadFieldMap(thread) +: channelFields) ++ methods,
-            Seq(),
-            BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
-        }
-      }
-    }
-    threadClasses
+  private def getThreadRunFromDecl(thread: VeyMontThread[Pre], decl: ClassDeclaration[Pre]): RunMethod[Post] = decl match {
+    case m: RunMethod[Pre] => getThreadRunMethod(m)
+    case _ => throw ParalliseVeyMontThreadsError(thread, "RunMethod expected in seq_program")
   }
 
-  private def getChannelFields(channelInfo: Seq[(Type[Pre], String, Statement[Pre])], channelClasses: Map[Type[Pre],JavaClass[Post]]): Seq[InstanceField[Post]] = {
-    channelInfo.map { case (chanType, chanName, assign) =>
-      new InstanceField[Post](JavaTClass(channelClasses(chanType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanName,assign)) }
+  private def generateThreadFields(seqProg: VeyMontSeqProg[Pre]) : Map[VeyMontThread[Pre],InstanceField[Post]] =
+    seqProg.threads.map { thread => (thread -> new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)) }.toMap
+
+  private def getChannelFields(channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[Ref[Pre, VeyMontThread[Pre]],InstanceField[Post]] = {
+    channelInfo.flatMap { chanInfo =>
+      val chanField = new InstanceField[Post](JavaTClass(channelClasses(chanInfo.channelType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanInfo.channelName,chanInfo.comExpr.assign))
+      Set((chanInfo.comExpr.receiver, chanField), (chanInfo.comExpr.sender, chanField)) }.toMap
   }
 
-  private def generateChannelClasses(channelInfo: Seq[(Type[Pre], String, Statement[Pre])]) : Map[Type[Pre],JavaClass[Post]] = {
-    val channelTypes = channelInfo.map(_._1).toSet
+  private def generateChannelClasses(channelInfo: Seq[ChannelInfo[Pre]]) : Map[Type[Pre],JavaClass[Post]] = {
+    val channelTypes = channelInfo.map(_.channelType).toSet
     channelTypes.map(channelType =>
       channelType -> {
         val chanClassPre = channelClass.asInstanceOf[JavaClass[Pre]]
@@ -121,9 +131,9 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
   }
 
-  private def getChannelNamesAndTypes(s: Statement[Pre]): Seq[(Type[Pre], String, Statement[Pre])] = {
+  private def getChannelNamesAndTypes(s: Statement[Pre]): Seq[ChannelInfo[Pre]] = {
     s.collect { case e@VeyMontCommExpression(recv, sender, assign) =>
-      (recv.decl.threadType, recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel", e)
+      new ChannelInfo(e,recv.decl.threadType, recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel")
     }
   }
 
@@ -137,6 +147,12 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         dispatch(method.contract))(method.blame)(method.o)
   }
 
+  private def getThreadRunMethod(run: RunMethod[Pre]): RunMethod[Post] = {
+    new RunMethod[Post](
+      run.body.map(dispatch),
+      dispatch(run.contract))(run.blame)(run.o)
+  }
+
 /*
   override def dispatch(st : Statement[Pre]) : Statement[Post] = {
     if (inSeqProg.nonEmpty) {
diff --git a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
new file mode 100644
index 0000000000..1a91662616
--- /dev/null
+++ b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
@@ -0,0 +1,9 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.{ClassDeclaration, InstanceField, Statement, VeyMontThread}
+import vct.col.ref.Ref
+import vct.col.rewrite.{Generation, Rewritten}
+
+class ThreadBuildingBlocks[Pre <: Generation](val runMethod: ClassDeclaration[Pre], val methods: Seq[ClassDeclaration[Pre]], val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]]) {
+
+}

From 05f14d6ccea3039664b4ee73869d17f74ef5abca Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 6 Jun 2023 13:45:51 +0200
Subject: [PATCH 07/20] edit

---
 .../vct/rewrite/veymont/ParalleliseVeyMontThreads.scala       | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 422e9a0f55..11ddd58b47 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -59,7 +59,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
             })
         }
       case thread: VeyMontThread[Pre] => {
-        if(threadBuildingBlocks.nonEmpty) {
+        if(threadBuildingBlocks.nonEmpty && inSeqProg.nonEmpty && inSeqProg.top == thread) {
           val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
           val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
           val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
@@ -73,7 +73,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
               (threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods),
               Seq(),
               BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
-            //globalDeclarations.declare(threadClass)
+            globalDeclarations.declare(threadClass)
           }
         } else rewriteDefault(thread)
       }

From 563d310a714476469274cc13ef030bf2a0c666ac Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 6 Jun 2023 17:20:50 +0200
Subject: [PATCH 08/20] busy fixing refs but not working yet

---
 .../veymont/ParalleliseVeyMontThreads.scala   | 79 +++++++++++--------
 .../veymont/ThreadBuildingBlocks.scala        |  6 +-
 2 files changed, 53 insertions(+), 32 deletions(-)

diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 11ddd58b47..617fde1457 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,11 +1,12 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.RewriteHelpers.RewriteJavaClass
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Eval, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, Node, Program, RunMethod, Scope, Statement, TClass, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
+import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
 import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelClassOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
 
@@ -43,25 +44,24 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
 
 case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] {
 
-  val inSeqProg: ScopedStack[VeyMontThread[Pre]] = ScopedStack()
+  val inSeqProg: ScopedStack[Map[VeyMontThread[Pre],InstanceField[Post]]] = ScopedStack()
   val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
+  val seqProgSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
+        val threadFieldMap = seqProg.threads.map(t => (t,new InstanceField[Post](dispatch(t.threadType), Set.empty)(t.o))).toMap
         val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
         val channelClasses = generateChannelClasses(channelInfo)
         val channelFields = getChannelFields(channelInfo, channelClasses)
-        threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods,channelFields)) {
-          seqProg.threads.foreach(t =>
-            inSeqProg.having(t) {
-              dispatch(t)
-            })
+        threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods,threadFieldMap,channelFields)) {
+          seqProg.threads.foreach(dispatch)
         }
       case thread: VeyMontThread[Pre] => {
-        if(threadBuildingBlocks.nonEmpty && inSeqProg.nonEmpty && inSeqProg.top == thread) {
-          val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+        if(threadBuildingBlocks.nonEmpty) {
           val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
+          val threadField = threadRes.threadFieldMap(thread)
           val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
             _.decl == thread
           }.values.toSeq
@@ -74,9 +74,12 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
               Seq(),
               BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
             globalDeclarations.declare(threadClass)
+            seqProgSucc.update(thread,threadClass)
           }
         } else rewriteDefault(thread)
       }
+      //case m: InstanceMethod[Pre] => getThreadMethod(m)
+      //case r: RunMethod[Pre] => getThreadRunMethod(r)
       case other => rewriteDefault(other)
     }
   }
@@ -91,9 +94,6 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     case _ => throw ParalliseVeyMontThreadsError(thread, "RunMethod expected in seq_program")
   }
 
-  private def generateThreadFields(seqProg: VeyMontSeqProg[Pre]) : Map[VeyMontThread[Pre],InstanceField[Post]] =
-    seqProg.threads.map { thread => (thread -> new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)) }.toMap
-
   private def getChannelFields(channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[Ref[Pre, VeyMontThread[Pre]],InstanceField[Post]] = {
     channelInfo.flatMap { chanInfo =>
       val chanField = new InstanceField[Post](JavaTClass(channelClasses(chanInfo.channelType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanInfo.channelName,chanInfo.comExpr.assign))
@@ -153,24 +153,41 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
       dispatch(run.contract))(run.blame)(run.o)
   }
 
-/*
-  override def dispatch(st : Statement[Pre]) : Statement[Post] = {
-    if (inSeqProg.nonEmpty) {
-      val thread = inSeqProg.top
-      val threadFieldMap = inSeqThreadMap.top
-      st match {
-        case VeyMontCommExpression(recv,sender,assign) => dispatch(assign)
-        case VeyMontAssignExpression(_, _) => rewriteDefault(st)
-        case Assign(_, _) => rewriteDefault(st)
-        case Branch(_) => rewriteDefault(st)
-        case Loop(_, _, _, _, _) => rewriteDefault(st)
-        case Scope(_, _) => rewriteDefault(st)
-        case Block(_) => rewriteDefault(st)
-        case Eval(expr) => dispatch(expr)
-        case Assert(_) => rewriteDefault(st)
-        case _ => throw VeyMontStructCheckError(st, "Statement not allowed in seq_program")
+  override def dispatch(node: Expr[Pre]): Expr[Post] = {
+    if(threadBuildingBlocks.nonEmpty) {
+      val threadFieldMap = threadBuildingBlocks.top.threadFieldMap
+      node match {
+        case d: Deref[Pre] => d.obj match {
+          case t: DerefVeyMontThread[Pre] =>
+            threadFieldMap.find{case (thread,_) => t.ref.decl == thread} match {
+              case Some((thread,threadField)) =>
+                d.rewrite(
+                  obj = Deref(ThisObject(seqProgSucc.ref[Post, Class[Post]](thread))(thread.o), threadField.ref[InstanceField[Post]])(null)(d.o)
+                )
+              case _ => rewriteDefault(node)
+            }
+        }
+        case _ => rewriteDefault(node)
       }
-    } else rewriteDefault(st)
+    } else rewriteDefault(node)
   }
-*/
+
+
+    override def dispatch(st : Statement[Pre]) : Statement[Post] = {
+      if (inSeqProg.nonEmpty) {
+        st match {
+          case VeyMontCommExpression(recv,sender,assign) => rewriteDefault(assign)
+          case VeyMontAssignExpression(_, _) => rewriteDefault(st)
+          case Assign(_, _) => rewriteDefault(st)
+          case Branch(_) => rewriteDefault(st)
+          case Loop(_, _, _, _, _) => rewriteDefault(st)
+          case Scope(_, _) => rewriteDefault(st)
+          case Block(_) => rewriteDefault(st)
+          case Eval(expr) => Eval(rewriteDefault(expr))(st.o)
+          case Assert(_) => rewriteDefault(st)
+          case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
+        }
+      } else rewriteDefault(st)
+    }
+
 }
diff --git a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
index 1a91662616..37eca91e8c 100644
--- a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
+++ b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
@@ -4,6 +4,10 @@ import vct.col.ast.{ClassDeclaration, InstanceField, Statement, VeyMontThread}
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewritten}
 
-class ThreadBuildingBlocks[Pre <: Generation](val runMethod: ClassDeclaration[Pre], val methods: Seq[ClassDeclaration[Pre]], val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]]) {
+class ThreadBuildingBlocks[Pre <: Generation](
+                                               val runMethod: ClassDeclaration[Pre],
+                                               val methods: Seq[ClassDeclaration[Pre]],
+                                               val threadFieldMap: Map[VeyMontThread[Pre],InstanceField[Rewritten[Pre]]],
+                                               val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]]) {
 
 }

From b3e4cfb1c2ea01b6158a3a4a30b6229e7bc4056a Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Wed, 7 Jun 2023 16:04:41 +0200
Subject: [PATCH 09/20] rewritting method call not working because overloaded
 dispatch for Ref

---
 src/col/vct/col/ast/Node.scala                |   1 +
 .../vct/col/typerules/CoercingRewriter.scala  |   1 +
 .../veymont/ParalleliseVeyMontThreads.scala   | 109 ++++++++++++------
 .../veymont/ThreadBuildingBlocks.scala        |   8 +-
 4 files changed, 82 insertions(+), 37 deletions(-)

diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index afb5c15f79..fc5922bc65 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -189,6 +189,7 @@ final case class WandApply[G](res: Expr[G])(val blame: Blame[WandApplyFailed])(i
 final case class Havoc[G](loc: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with HavocImpl[G]
 final case class FramedProof[G](pre: Expr[G], body: Statement[G], post: Expr[G])(val blame: Blame[FramedProofFailure])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FramedProofImpl[G]
 final case class Extract[G](contractedStatement: Statement[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with ExtractImpl[G]
+final case class Skip[G]()(implicit val o: Origin) extends NormallyCompletingStatement[G]
 
 sealed trait ExceptionalStatement[G] extends Statement[G] with ExceptionalStatementImpl[G]
 final case class Eval[G](expr: Expr[G])(implicit val o: Origin) extends ExceptionalStatement[G] with EvalImpl[G]
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 21984d108d..149c959e5c 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1574,6 +1574,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case ass @ SilverFieldAssign(obj, field, value) => SilverFieldAssign(ref(obj), field, coerce(value, field.decl.t))(ass.blame)
       case SilverLocalAssign(v, value) => SilverLocalAssign(v, coerce(value, v.decl.t))
       case SilverNewRef(v, fields) => SilverNewRef(v, fields)
+      case Skip() => Skip()
       case SpecIgnoreEnd() => SpecIgnoreEnd()
       case SpecIgnoreStart() => SpecIgnoreStart()
       case Switch(expr, body) => Switch(expr, body)
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 617fde1457..e5345cac30 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -2,14 +2,16 @@ package vct.rewrite.veymont
 
 import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
 import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelClassOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
 
+import scala.collection.immutable.Seq
+
 object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   override def key: String = "ParalleliseVeyMontThreads"
 
@@ -44,38 +46,27 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
 
 case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] {
 
-  val inSeqProg: ScopedStack[Map[VeyMontThread[Pre],InstanceField[Post]]] = ScopedStack()
-  val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
-  val seqProgSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
+  private val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
+  private val threadClassSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
+  private val threadMethodSucc: SuccessionMap[(VeyMontThread[Pre],ClassDeclaration[Pre]),InstanceMethod[Post]] = SuccessionMap()
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
-        val threadFieldMap = seqProg.threads.map(t => (t,new InstanceField[Post](dispatch(t.threadType), Set.empty)(t.o))).toMap
         val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
         val channelClasses = generateChannelClasses(channelInfo)
         val channelFields = getChannelFields(channelInfo, channelClasses)
-        threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods,threadFieldMap,channelFields)) {
-          seqProg.threads.foreach(dispatch)
-        }
+        seqProg.threads.foreach(thread => {
+          val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+          threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
+            dispatch(thread)
+          }
+        })
       case thread: VeyMontThread[Pre] => {
         if(threadBuildingBlocks.nonEmpty) {
           val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
-          val threadField = threadRes.threadFieldMap(thread)
-          val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
-            _.decl == thread
-          }.values.toSeq
-          val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
-          val threadMethods: Seq[ClassDeclaration[Post]] = threadRes.methods.map(getThreadMethodFromDecl(thread))
-          classDeclarations.scope {
-            //classDeclarations.collect {
-            val threadClass = new Class[Post](
-              (threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods),
-              Seq(),
-              BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
-            globalDeclarations.declare(threadClass)
-            seqProgSucc.update(thread,threadClass)
-          }
+          val threadMethods: Seq[ClassDeclaration[Post]] = createThreadMethod(thread, threadRes)
+          createThreadClass(thread, threadRes, threadMethods)
         } else rewriteDefault(thread)
       }
       //case m: InstanceMethod[Pre] => getThreadMethod(m)
@@ -84,6 +75,30 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
   }
 
+  private def createThreadMethod(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre]) = {
+    threadRes.methods.map { preMethod =>
+      val postMethod = getThreadMethodFromDecl(thread)(preMethod)
+      threadMethodSucc.update((thread, preMethod), postMethod)
+      postMethod
+    }
+  }
+
+  private def createThreadClass(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre], threadMethods: Seq[ClassDeclaration[Post]]): Unit = {
+    val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
+      _.decl == thread
+    }.values.toSeq
+    val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
+    classDeclarations.scope {
+      //classDeclarations.collect {
+      val threadClass = new Class[Post](
+        (threadRes.threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods),
+        Seq(),
+        BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
+      globalDeclarations.declare(threadClass)
+      threadClassSucc.update(thread, threadClass)
+    }
+  }
+
   private def getThreadMethodFromDecl(thread: VeyMontThread[Pre])(decl: ClassDeclaration[Pre]): InstanceMethod[Post]  = decl match {
     case m: InstanceMethod[Pre] => getThreadMethod(m)
     case _ => throw ParalliseVeyMontThreadsError(thread, "Methods of seq_program need to be of type InstanceMethod")
@@ -155,17 +170,32 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
 
   override def dispatch(node: Expr[Pre]): Expr[Post] = {
     if(threadBuildingBlocks.nonEmpty) {
-      val threadFieldMap = threadBuildingBlocks.top.threadFieldMap
+      val thread = threadBuildingBlocks.top.thread
       node match {
+        case c: VeyMontCondition[Pre] => c.condition.find{ case (threadRef,_) =>
+          threadRef.decl == thread
+        } match {
+          case Some((_,threadExpr)) => dispatch(threadExpr)
+          case _ => throw ParalliseVeyMontThreadsError(node, "Condition of if statement or while loop must contain an expression for every thread")
+        }
+        case m: MethodInvocation[Pre] => threadMethodSucc.get((thread,m.ref.decl)) match {
+          case Some(postMethod) => MethodInvocation[Post](dispatch(m.obj),postMethod.ref,m.args.map(dispatch),
+            m.outArgs.map(dispatch),m.typeArgs.map(dispatch),
+            m.givenMap.map{ case (r,e) => (dispatch(r),dispatch(e))},
+            m.yields.map{case (e,r) => (dispatch(e),dispatch(r))})(m.blame)(m.o)
+          case None => throw ParalliseVeyMontThreadsError(m,"No successor for this method found")
+        }
+        case t: ThisObject[Pre] => ThisObject(threadClassSucc.ref[Post, Class[Post]](threadBuildingBlocks.top.thread))(threadBuildingBlocks.top.thread.o)
         case d: Deref[Pre] => d.obj match {
           case t: DerefVeyMontThread[Pre] =>
-            threadFieldMap.find{case (thread,_) => t.ref.decl == thread} match {
-              case Some((thread,threadField)) =>
-                d.rewrite(
-                  obj = Deref(ThisObject(seqProgSucc.ref[Post, Class[Post]](thread))(thread.o), threadField.ref[InstanceField[Post]])(null)(d.o)
-                )
-              case _ => rewriteDefault(node)
+            val threadField = threadBuildingBlocks.top.threadField
+            if(t.ref.decl == thread) {
+              d.rewrite(
+                obj = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), threadField.ref[InstanceField[Post]])(null)(d.o)
+              )
             }
+            else rewriteDefault(node)
+
         }
         case _ => rewriteDefault(node)
       }
@@ -174,10 +204,21 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
 
 
     override def dispatch(st : Statement[Pre]) : Statement[Post] = {
-      if (inSeqProg.nonEmpty) {
+      if (threadBuildingBlocks.nonEmpty) {
+        val thread = threadBuildingBlocks.top.thread
         st match {
-          case VeyMontCommExpression(recv,sender,assign) => rewriteDefault(assign)
-          case VeyMontAssignExpression(_, _) => rewriteDefault(st)
+          case VeyMontCommExpression(recv,sender,assign) =>
+            if (recv.decl == thread)
+              dispatch(assign)
+            else if(sender.decl == thread) {
+              //MethodInvocation(dispatch(sender),)
+              dispatch(assign)
+            }
+            else Skip()(assign.o)
+          case VeyMontAssignExpression(threadRef, assign) =>
+            if (threadRef.decl == thread)
+              dispatch(assign)
+            else Skip()(assign.o)
           case Assign(_, _) => rewriteDefault(st)
           case Branch(_) => rewriteDefault(st)
           case Loop(_, _, _, _, _) => rewriteDefault(st)
diff --git a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
index 37eca91e8c..b9840dbab4 100644
--- a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
+++ b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
@@ -1,13 +1,15 @@
 package vct.rewrite.veymont
 
-import vct.col.ast.{ClassDeclaration, InstanceField, Statement, VeyMontThread}
+import vct.col.ast.{ClassDeclaration, InstanceField, JavaClass, Statement, Type, VeyMontThread}
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewritten}
 
 class ThreadBuildingBlocks[Pre <: Generation](
                                                val runMethod: ClassDeclaration[Pre],
                                                val methods: Seq[ClassDeclaration[Pre]],
-                                               val threadFieldMap: Map[VeyMontThread[Pre],InstanceField[Rewritten[Pre]]],
-                                               val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]]) {
+                                               val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]],
+                                               val channelClasses: Map[Type[Pre],JavaClass[Rewritten[Pre]]],
+                                               val thread: VeyMontThread[Pre],
+                                               val threadField: InstanceField[Rewritten[Pre]]) {
 
 }

From f362bdc2260f4c84095e1b1a75e79b8197d2f492 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Mon, 12 Jun 2023 14:32:29 +0200
Subject: [PATCH 10/20] rewriting method call works

---
 .../veymont/ParalleliseVeyMontThreads.scala      | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index e5345cac30..da4cee9d0c 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,7 +1,7 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass}
+import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
 import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
@@ -178,12 +178,12 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
           case Some((_,threadExpr)) => dispatch(threadExpr)
           case _ => throw ParalliseVeyMontThreadsError(node, "Condition of if statement or while loop must contain an expression for every thread")
         }
-        case m: MethodInvocation[Pre] => threadMethodSucc.get((thread,m.ref.decl)) match {
-          case Some(postMethod) => MethodInvocation[Post](dispatch(m.obj),postMethod.ref,m.args.map(dispatch),
-            m.outArgs.map(dispatch),m.typeArgs.map(dispatch),
-            m.givenMap.map{ case (r,e) => (dispatch(r),dispatch(e))},
-            m.yields.map{case (e,r) => (dispatch(e),dispatch(r))})(m.blame)(m.o)
-          case None => throw ParalliseVeyMontThreadsError(m,"No successor for this method found")
+        case m: MethodInvocation[Pre] => m.obj match {
+          case threadRef: DerefVeyMontThread[Pre] => m.rewrite(obj = dispatch(threadRef))
+          case _ => threadMethodSucc.get((thread, m.ref.decl)) match {
+            case Some(postMethod) => m.rewrite(obj = dispatch(m.obj), ref = postMethod.ref, m.args.map(dispatch))
+            case None => throw ParalliseVeyMontThreadsError(m, "No successor for this method found")
+          }
         }
         case t: ThisObject[Pre] => ThisObject(threadClassSucc.ref[Post, Class[Post]](threadBuildingBlocks.top.thread))(threadBuildingBlocks.top.thread.o)
         case d: Deref[Pre] => d.obj match {
@@ -224,7 +224,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
           case Loop(_, _, _, _, _) => rewriteDefault(st)
           case Scope(_, _) => rewriteDefault(st)
           case Block(_) => rewriteDefault(st)
-          case Eval(expr) => Eval(rewriteDefault(expr))(st.o)
+          case Eval(expr) => Eval(dispatch(expr))(st.o)
           case Assert(_) => rewriteDefault(st)
           case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
         }

From a30bf5dfaab29c5c7c40a5e1c79333b151449d3b Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 13 Jun 2023 17:15:24 +0200
Subject: [PATCH 11/20] working on rewriting VeyMont Comm Expr

---
 src/col/vct/col/ast/Node.scala                |  2 +-
 .../vct/col/typerules/CoercingRewriter.scala  |  2 +-
 .../veymont/AddVeyMontAssignmentNodes.scala   |  2 +-
 .../veymont/ParalleliseVeyMontThreads.scala   | 36 +++++++++++++------
 .../veymont/ThreadBuildingBlocks.scala        |  5 +--
 5 files changed, 31 insertions(+), 16 deletions(-)

diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index fc5922bc65..9c066f1b7d 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -671,7 +671,7 @@ final case class SuperType[G](left: Expr[G], right: Expr[G])(implicit val o: Ori
 final case class IndeterminateInteger[G](min: Expr[G], max: Expr[G])(implicit val o: Origin) extends Expr[G] with IndeterminateIntegerImpl[G]
 
 sealed trait AssignExpression[G] extends Expr[G] with AssignExpressionImpl[G]
-final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
+final case class VeyMontCommExpression[G](receiver: Ref[G,VeyMontThread[G]], sender : Ref[G,VeyMontThread[G]], chanType: Type[G], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontCommImpl[G]
 final case class VeyMontAssignExpression[G](thread : Ref[G,VeyMontThread[G]], assign: Statement[G])(implicit val o: Origin) extends Statement[G] with VeyMontAssignExpressionImpl[G]
 final case class PreAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PreAssignExpressionImpl[G]
 final case class PostAssignExpression[G](target: Expr[G], value: Expr[G])(val blame: Blame[AssignFailed])(implicit val o: Origin) extends AssignExpression[G] with PostAssignExpressionImpl[G]
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 149c959e5c..99fd2b8945 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1588,7 +1588,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case w @ WandApply(assn) => WandApply(res(assn))(w.blame)
       case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
       case VeyMontAssignExpression(t,a) => VeyMontAssignExpression(t,a)
-      case VeyMontCommExpression(r,s,a) => VeyMontCommExpression(r,s,a)
+      case VeyMontCommExpression(r,s,t,a) => VeyMontCommExpression(r,s,t,a)
     }
   }
 
diff --git a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala b/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
index f3c19ff228..b5411730e8 100644
--- a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
+++ b/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
@@ -93,7 +93,7 @@ case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre]
       new VeyMontAssignExpression[Post](succ(receiver), rewriteDefault(a))(a.o)
     else if (derefs.size == 1) {
       val sender = getAssignmentSender(derefs.head)
-      new VeyMontCommExpression[Post](succ(receiver), succ(sender), rewriteDefault(a))(a.o)
+      new VeyMontCommExpression[Post](succ(receiver), succ(sender), dispatch(derefs.head.ref.decl.t), rewriteDefault(a))(a.o)
     } else throw AddVeyMontAssignmentError(a.value, "The value of this assignment is not allowed to refer to multiple threads!")
   }
 
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index da4cee9d0c..f435ab9a37 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -2,7 +2,7 @@ package vct.rewrite.veymont
 
 import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
@@ -54,8 +54,11 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
         val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
-        val channelClasses = generateChannelClasses(channelInfo)
-        val channelFields = getChannelFields(channelInfo, channelClasses)
+        val indexedChannelInfo : Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
+          if (chanInfoSeq.size <= 1) chanInfoSeq
+          else chanInfoSeq.zipWithIndex.map{ case (chanInfo,index) => new ChannelInfo(chanInfo.comExpr,chanInfo.channelType,chanInfo.channelName + index) }).toSeq
+        val channelClasses = generateChannelClasses(indexedChannelInfo)
+        val channelFields = getChannelFields(indexedChannelInfo, channelClasses)
         seqProg.threads.foreach(thread => {
           val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
           threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
@@ -109,10 +112,10 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     case _ => throw ParalliseVeyMontThreadsError(thread, "RunMethod expected in seq_program")
   }
 
-  private def getChannelFields(channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[Ref[Pre, VeyMontThread[Pre]],InstanceField[Post]] = {
-    channelInfo.flatMap { chanInfo =>
+  private def getChannelFields(channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[(VeyMontCommExpression[Pre],Origin),InstanceField[Post]] = {
+    channelInfo.map { chanInfo =>
       val chanField = new InstanceField[Post](JavaTClass(channelClasses(chanInfo.channelType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanInfo.channelName,chanInfo.comExpr.assign))
-      Set((chanInfo.comExpr.receiver, chanField), (chanInfo.comExpr.sender, chanField)) }.toMap
+      ((chanInfo.comExpr,chanInfo.comExpr.o), chanField) }.toMap
   }
 
   private def generateChannelClasses(channelInfo: Seq[ChannelInfo[Pre]]) : Map[Type[Pre],JavaClass[Post]] = {
@@ -147,8 +150,8 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   }
 
   private def getChannelNamesAndTypes(s: Statement[Pre]): Seq[ChannelInfo[Pre]] = {
-    s.collect { case e@VeyMontCommExpression(recv, sender, assign) =>
-      new ChannelInfo(e,recv.decl.threadType, recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel")
+    s.collect { case e@VeyMontCommExpression(recv, sender, chanType, assign) =>
+      new ChannelInfo(e,chanType, recv.decl.o.preferredName + sender.decl.o.preferredName + "Channel")
     }
   }
 
@@ -207,12 +210,16 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
       if (threadBuildingBlocks.nonEmpty) {
         val thread = threadBuildingBlocks.top.thread
         st match {
-          case VeyMontCommExpression(recv,sender,assign) =>
+          case v@VeyMontCommExpression(recv,sender,chanType,assign) =>
+            val channelField = threadBuildingBlocks.top.channelFields((v,v.o))
+            val channelClass = threadBuildingBlocks.top.channelClasses(chanType)
+            val assignment = assign.asInstanceOf[Assign[Pre]]
             if (recv.decl == thread)
               dispatch(assign)
             else if(sender.decl == thread) {
-              //MethodInvocation(dispatch(sender),)
-              dispatch(assign)
+              val writeMethod = findChannelClassMethod(v, channelClass, "writeValue")
+              val thisChanField = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), channelField.ref[InstanceField[Post]])(null)(assign.o)
+              Eval(MethodInvocation(thisChanField,writeMethod.ref[InstanceMethod[Post]],Seq(dispatch(assignment.value)),Seq.empty,Seq.empty,Seq.empty,Seq.empty)(null)(v.o))(v.o)
             }
             else Skip()(assign.o)
           case VeyMontAssignExpression(threadRef, assign) =>
@@ -231,4 +238,11 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
       } else rewriteDefault(st)
     }
 
+  private def findChannelClassMethod(v: VeyMontCommExpression[Pre], channelClass: JavaClass[Post], methodName: String) = {
+    val writeMethod = channelClass.decls.find { case m: InstanceMethod[Pre] => m.o.preferredName == methodName } match {
+      case Some(m: InstanceMethod[Post]) => m
+      case _ => throw ParalliseVeyMontThreadsError(v, "Could not find method `" + methodName + "' for channelClass")
+    }
+    writeMethod
+  }
 }
diff --git a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
index b9840dbab4..89140d8ec2 100644
--- a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
+++ b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
@@ -1,13 +1,14 @@
 package vct.rewrite.veymont
 
-import vct.col.ast.{ClassDeclaration, InstanceField, JavaClass, Statement, Type, VeyMontThread}
+import vct.col.ast.{ClassDeclaration, InstanceField, JavaClass, Statement, Type, VeyMontCommExpression, VeyMontThread}
+import vct.col.origin.Origin
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewritten}
 
 class ThreadBuildingBlocks[Pre <: Generation](
                                                val runMethod: ClassDeclaration[Pre],
                                                val methods: Seq[ClassDeclaration[Pre]],
-                                               val channelFields: Map[Ref[Pre,VeyMontThread[Pre]],InstanceField[Rewritten[Pre]]],
+                                               val channelFields: Map[(VeyMontCommExpression[Pre],Origin),InstanceField[Rewritten[Pre]]],
                                                val channelClasses: Map[Type[Pre],JavaClass[Rewritten[Pre]]],
                                                val thread: VeyMontThread[Pre],
                                                val threadField: InstanceField[Rewritten[Pre]]) {

From f4961fc4e71166895ce8f175d121dbd6035189db Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Fri, 16 Jun 2023 16:00:03 +0200
Subject: [PATCH 12/20] rewriting of statements working but channel class type
 is not rewritten

---
 .../veymont-seq-progs/veymont-swap.pvl        |  2 +-
 .../veymont/AddVeyMontAssignmentNodes.scala   | 12 ++++-
 .../veymont/ParalleliseVeyMontThreads.scala   | 54 ++++++++++++-------
 .../vct/rewrite/veymont/StructureCheck.scala  |  2 +-
 4 files changed, 48 insertions(+), 22 deletions(-)

diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/examples/technical/veymont-seq-progs/veymont-swap.pvl
index a4d40454c8..471c083458 100644
--- a/examples/technical/veymont-seq-progs/veymont-swap.pvl
+++ b/examples/technical/veymont-seq-progs/veymont-swap.pvl
@@ -25,7 +25,7 @@ seq_program SeqProgram(int x, int y) {
   int num() {}
   
   void foo() {
-     s1.temp = 5;
+     s1.temp = 7;
   }
   
   //void bar(int a) {}
diff --git a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala b/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
index b5411730e8..1b0bf1bbaa 100644
--- a/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
+++ b/src/rewrite/vct/rewrite/veymont/AddVeyMontAssignmentNodes.scala
@@ -92,8 +92,16 @@ case class AddVeyMontAssignmentNodes[Pre <: Generation]() extends Rewriter[Pre]
     if (derefs.isEmpty)
       new VeyMontAssignExpression[Post](succ(receiver), rewriteDefault(a))(a.o)
     else if (derefs.size == 1) {
-      val sender = getAssignmentSender(derefs.head)
-      new VeyMontCommExpression[Post](succ(receiver), succ(sender), dispatch(derefs.head.ref.decl.t), rewriteDefault(a))(a.o)
+      val thread = derefs.head.obj match {
+        case t: DerefVeyMontThread[Pre] => t
+        case _ => throw AddVeyMontAssignmentError(a.value, "The value of this assignment is expected to be a Deref of a thread!")
+      }
+      if(thread.ref.decl == receiver)
+        new VeyMontAssignExpression[Post](succ(receiver),rewriteDefault(a))(a.o)
+      else {
+        val sender = getAssignmentSender(derefs.head)
+        new VeyMontCommExpression[Post](succ(receiver), succ(sender), dispatch(derefs.head.ref.decl.t), rewriteDefault(a))(a.o)
+      }
     } else throw AddVeyMontAssignmentError(a.value, "The value of this assignment is not allowed to refer to multiple threads!")
   }
 
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index f435ab9a37..6463da6c60 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,10 +1,13 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast
+import vct.col.ast.RewriteHelpers.{RewriteAssign, RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
+import vct.col.resolve.ctx.RefJavaMethod
+import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.getDerefsFromExpr
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
@@ -88,7 +91,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
 
   private def createThreadClass(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre], threadMethods: Seq[ClassDeclaration[Post]]): Unit = {
     val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
-      _.decl == thread
+      case (comExpr,_) => comExpr.receiver.decl == thread || comExpr.sender.decl == thread
     }.values.toSeq
     val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
     classDeclarations.scope {
@@ -188,7 +191,6 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
             case None => throw ParalliseVeyMontThreadsError(m, "No successor for this method found")
           }
         }
-        case t: ThisObject[Pre] => ThisObject(threadClassSucc.ref[Post, Class[Post]](threadBuildingBlocks.top.thread))(threadBuildingBlocks.top.thread.o)
         case d: Deref[Pre] => d.obj match {
           case t: DerefVeyMontThread[Pre] =>
             val threadField = threadBuildingBlocks.top.threadField
@@ -213,36 +215,52 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
           case v@VeyMontCommExpression(recv,sender,chanType,assign) =>
             val channelField = threadBuildingBlocks.top.channelFields((v,v.o))
             val channelClass = threadBuildingBlocks.top.channelClasses(chanType)
+            val thisChanField = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), channelField.ref[InstanceField[Post]])(null)(assign.o)
             val assignment = assign.asInstanceOf[Assign[Pre]]
-            if (recv.decl == thread)
-              dispatch(assign)
-            else if(sender.decl == thread) {
+            if (recv.decl == thread) {
+              val readMethod = findChannelClassMethod(v, channelClass, "readValue")
+              val assignValue = JavaInvocation(Some(thisChanField),Seq.empty, "readValue",Seq.empty, Seq.empty,Seq.empty)(null)(v.o)
+              assignValue.ref = Some(RefJavaMethod(readMethod))
+              Assign(dispatch(assignment.target),assignValue)(null)(v.o)
+            } else if(sender.decl == thread) {
               val writeMethod = findChannelClassMethod(v, channelClass, "writeValue")
-              val thisChanField = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), channelField.ref[InstanceField[Post]])(null)(assign.o)
-              Eval(MethodInvocation(thisChanField,writeMethod.ref[InstanceMethod[Post]],Seq(dispatch(assignment.value)),Seq.empty,Seq.empty,Seq.empty,Seq.empty)(null)(v.o))(v.o)
+              val writeInvoc = JavaInvocation(Some(thisChanField),Seq.empty,"writeValue",Seq(dispatch(assignment.value)),Seq.empty,Seq.empty)(null)(v.o)
+              writeInvoc.ref = Some(RefJavaMethod(writeMethod))
+              Eval(writeInvoc)(v.o)
             }
             else Skip()(assign.o)
-          case VeyMontAssignExpression(threadRef, assign) =>
+          case v@VeyMontAssignExpression(threadRef, assign) =>
             if (threadRef.decl == thread)
               dispatch(assign)
             else Skip()(assign.o)
-          case Assign(_, _) => rewriteDefault(st)
+          case a: Assign[Pre] => rewriteDefault(st)
           case Branch(_) => rewriteDefault(st)
           case Loop(_, _, _, _, _) => rewriteDefault(st)
           case Scope(_, _) => rewriteDefault(st)
           case Block(_) => rewriteDefault(st)
-          case Eval(expr) => Eval(dispatch(expr))(st.o)
-          case Assert(_) => rewriteDefault(st)
+          case Eval(expr) => expr match {
+            case m: MethodInvocation[Pre] => m.obj match {
+              case _: ThisSeqProg[Pre] => Eval(dispatch(expr))(st.o)
+              case d: DerefVeyMontThread[Pre] => if(d.ref.decl == thread) Eval(dispatch(expr))(st.o) else Skip()(st.o)
+              case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
+            }
+            case _ => rewriteDefault(st)
+          }
+          case _: Assert[Pre] => Skip()(st.o)
           case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
         }
       } else rewriteDefault(st)
     }
 
-  private def findChannelClassMethod(v: VeyMontCommExpression[Pre], channelClass: JavaClass[Post], methodName: String) = {
-    val writeMethod = channelClass.decls.find { case m: InstanceMethod[Pre] => m.o.preferredName == methodName } match {
-      case Some(m: InstanceMethod[Post]) => m
-      case _ => throw ParalliseVeyMontThreadsError(v, "Could not find method `" + methodName + "' for channelClass")
+  private def findChannelClassMethod(v: VeyMontCommExpression[Pre], channelClass: JavaClass[Post], methodName: String): JavaMethod[Post] = {
+    val method = channelClass.decls.find {
+      case jm: JavaMethod[Post] => jm.name == methodName
+      case _ => false
+    }
+    method match {
+      case Some(m : JavaMethod[Post]) => m
+      case _ => throw ParalliseVeyMontThreadsError(v, "Could not find method `" + methodName + "' for channel class " + channelClass.name)
     }
-    writeMethod
   }
+
 }
diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
index 3ec673277d..8af88c94f6 100644
--- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
+++ b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
@@ -56,7 +56,7 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
   override def dispatch(st : Statement[Pre]) : Statement[Post] = {
     if(inSeqProg.nonEmpty)
       st match {
-        case VeyMontCommExpression(_,_,_) => rewriteDefault(st)
+        case VeyMontCommExpression(_,_,_,_) => rewriteDefault(st)
         case VeyMontAssignExpression(_,_) => rewriteDefault (st)
         case Assign(_,_) => rewriteDefault (st)
         case Branch(_) => rewriteDefault(st)

From 6c93b76c0b2305cc1afb1df3699dfdebbb6c7410 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 27 Jun 2023 13:57:44 +0200
Subject: [PATCH 13/20] rewriting MessageType now compiling

---
 src/main/vct/main/stages/Transformation.scala |  2 +-
 .../veymont/ChannelClassGenerator.scala       | 21 ----------------
 .../veymont/ParalleliseVeyMontThreads.scala   | 24 +++++++++++++++----
 3 files changed, 20 insertions(+), 27 deletions(-)
 delete mode 100644 src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala

diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index 96681e195a..ad04613619 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -22,7 +22,7 @@ import vct.options.Options
 import vct.options.types.{Backend, PathOrStd}
 import vct.resources.Resources
 import vct.result.VerificationError.SystemError
-import vct.rewrite.veymont.{ChannelClassGenerator, ParalleliseVeyMontThreads}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads
 
 object Transformation {
   case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[CheckError]) extends SystemError {
diff --git a/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala b/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala
deleted file mode 100644
index 71f26d53d4..0000000000
--- a/src/rewrite/vct/rewrite/veymont/ChannelClassGenerator.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-package vct.rewrite.veymont
-
-import vct.col.ast.Type
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg}
-
-object ChannelClassGenerator extends RewriterBuilderArg[Type[_]] {
-  override def key: String = "ChannelClassGenerator"
-
-  override def desc: String = "Generate classes for channels of a VeyMont seq_program"
-
-}
-
-case class ChannelClassGenerator [Pre <: Generation](channelType: Type[_]) extends Rewriter[Pre] {
-
-  override def dispatch(t: Type[Pre]) : Type[Post] = {
-    if(t.o.preferredName == "MessageType")
-      dispatch(channelType.asInstanceOf[Type[Pre]])
-    else rewriteDefault(t)
-  }
-
-}
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 6463da6c60..3a747e4731 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -3,7 +3,7 @@ package vct.rewrite.veymont
 import hre.util.ScopedStack
 import vct.col.ast
 import vct.col.ast.RewriteHelpers.{RewriteAssign, RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.RefJavaMethod
@@ -47,7 +47,7 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   }
 }
 
-case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] {
+case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] { outer =>
 
   private val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
   private val threadClassSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
@@ -126,12 +126,26 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     channelTypes.map(channelType =>
       channelType -> {
         val chanClassPre = channelClass.asInstanceOf[JavaClass[Pre]]
-        new RewriteJavaClass[Pre, Post](chanClassPre)(new ChannelClassGenerator[Pre](channelType)).rewrite(decls = classDeclarations.collect {
-          chanClassPre.decls.foreach(d => dispatch(d))
+        val rw = new ChannelClassGenerator(channelType)
+        new RewriteJavaClass[Pre, Post](chanClassPre)(rw).rewrite(decls = classDeclarations.collect {
+          chanClassPre.decls.foreach(d => rw.dispatch(d))
         }._1)
       }
     ).toMap
-  }//new ChannelClassGenerator(channelType).globalDeclarations.dispatch(channelClass.unsafeTransmuteGeneration[JavaClass, Pre])
+  }
+
+  case class ChannelClassGenerator(channelType: Type[_]) extends Rewriter[Pre] {
+    override val allScopes = outer.allScopes
+
+    override def dispatch(t: Type[Pre]): Type[Post] = t match {
+      //  case jt: JavaType[Pre] => jt match {
+      case jnt: JavaNamedType[Pre] =>
+        if (jnt.names.head._1 == "MessageType") {
+          dispatch(channelType.asInstanceOf[Type[Pre]])
+        } else rewriteDefault(jnt)
+      case _ => rewriteDefault(t)
+    }
+  }
 
   private def collectChannelsFromRun(seqProg: VeyMontSeqProg[Pre]) =
     seqProg.runMethod match {

From 8cb1d51bf0089f298c35cf26f99d4d54c278fa90 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 4 Jul 2023 15:20:48 +0200
Subject: [PATCH 14/20] method invokation refs fixed

---
 .../ParallelCommExprBuildingBlocks.scala      |   9 +
 .../veymont/ParalleliseVeyMontThreads.scala   | 197 +++++++++++-------
 .../veymont/ThreadBuildingBlocks.scala        |   3 +-
 3 files changed, 128 insertions(+), 81 deletions(-)
 create mode 100644 src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala

diff --git a/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala
new file mode 100644
index 0000000000..9faf3047be
--- /dev/null
+++ b/src/rewrite/vct/rewrite/veymont/ParallelCommExprBuildingBlocks.scala
@@ -0,0 +1,9 @@
+package vct.rewrite.veymont
+
+import vct.col.ast.{Assign, Deref, InstanceField, JavaClass}
+import vct.col.rewrite.{Generation, Rewritten}
+
+class ParallelCommExprBuildingBlocks[Pre <: Generation](val channelField: InstanceField[Rewritten[Pre]], val channelClass: JavaClass[Rewritten[Pre]],
+                                                         val thisChanField: Deref[Rewritten[Pre]], val assign: Assign[Pre] ) {
+
+}
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 3a747e4731..3e13008df4 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -3,7 +3,7 @@ package vct.rewrite.veymont
 import hre.util.ScopedStack
 import vct.col.ast
 import vct.col.ast.RewriteHelpers.{RewriteAssign, RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Skip, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.{Origin, PreferredNameOrigin}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.RefJavaMethod
@@ -56,31 +56,42 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case seqProg: VeyMontSeqProg[Pre] =>
-        val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
-        val indexedChannelInfo : Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
-          if (chanInfoSeq.size <= 1) chanInfoSeq
-          else chanInfoSeq.zipWithIndex.map{ case (chanInfo,index) => new ChannelInfo(chanInfo.comExpr,chanInfo.channelType,chanInfo.channelName + index) }).toSeq
-        val channelClasses = generateChannelClasses(indexedChannelInfo)
-        val channelFields = getChannelFields(indexedChannelInfo, channelClasses)
-        seqProg.threads.foreach(thread => {
-          val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
-          threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
-            dispatch(thread)
-          }
-        })
+        val (channelClasses,channelFields) = extractChannelInfo(seqProg)
+        dispatchThreads(seqProg, channelClasses, channelFields)
       case thread: VeyMontThread[Pre] => {
-        if(threadBuildingBlocks.nonEmpty) {
-          val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
-          val threadMethods: Seq[ClassDeclaration[Post]] = createThreadMethod(thread, threadRes)
-          createThreadClass(thread, threadRes, threadMethods)
-        } else rewriteDefault(thread)
+        dispatchThread(thread)
       }
-      //case m: InstanceMethod[Pre] => getThreadMethod(m)
-      //case r: RunMethod[Pre] => getThreadRunMethod(r)
       case other => rewriteDefault(other)
     }
   }
 
+  private def dispatchThread(thread: VeyMontThread[Pre]): Unit = {
+    if (threadBuildingBlocks.nonEmpty) {
+      val threadRes: ThreadBuildingBlocks[Pre] = threadBuildingBlocks.top
+      val threadMethods: Seq[ClassDeclaration[Post]] = createThreadMethod(thread, threadRes)
+      createThreadClass(thread, threadRes, threadMethods)
+    } else rewriteDefault(thread)
+  }
+
+  private def dispatchThreads(seqProg: VeyMontSeqProg[Pre], channelClasses: Map[Type[Pre], JavaClass[Post]], channelFields: Map[(VeyMontCommExpression[Pre], Origin), InstanceField[Post]]): Unit = {
+    seqProg.threads.foreach(thread => {
+      val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+      threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
+        dispatch(thread)
+      }
+    })
+  }
+
+  private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Map[(VeyMontCommExpression[Pre], Origin), InstanceField[Post]]) = {
+    val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
+    val indexedChannelInfo: Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
+      if (chanInfoSeq.size <= 1) chanInfoSeq
+      else chanInfoSeq.zipWithIndex.map { case (chanInfo, index) => new ChannelInfo(chanInfo.comExpr, chanInfo.channelType, chanInfo.channelName + index) }).toSeq
+    val channelClasses = generateChannelClasses(indexedChannelInfo)
+    val channelFields = getChannelFields(indexedChannelInfo, channelClasses)
+    (channelClasses, channelFields)
+  }
+
   private def createThreadMethod(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre]) = {
     threadRes.methods.map { preMethod =>
       val postMethod = getThreadMethodFromDecl(thread)(preMethod)
@@ -95,11 +106,8 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }.values.toSeq
     val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
     classDeclarations.scope {
-      //classDeclarations.collect {
       val threadClass = new Class[Post](
-        (threadRes.threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods),
-        Seq(),
-        BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
+        (threadRes.threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods), Seq(), BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
       globalDeclarations.declare(threadClass)
       threadClassSucc.update(thread, threadClass)
     }
@@ -126,7 +134,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     channelTypes.map(channelType =>
       channelType -> {
         val chanClassPre = channelClass.asInstanceOf[JavaClass[Pre]]
-        val rw = new ChannelClassGenerator(channelType)
+        val rw = ChannelClassGenerator(channelType)
         new RewriteJavaClass[Pre, Post](chanClassPre)(rw).rewrite(decls = classDeclarations.collect {
           chanClassPre.decls.foreach(d => rw.dispatch(d))
         }._1)
@@ -138,7 +146,6 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     override val allScopes = outer.allScopes
 
     override def dispatch(t: Type[Pre]): Type[Post] = t match {
-      //  case jt: JavaType[Pre] => jt match {
       case jnt: JavaNamedType[Pre] =>
         if (jnt.names.head._1 == "MessageType") {
           dispatch(channelType.asInstanceOf[Type[Pre]])
@@ -192,80 +199,112 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     if(threadBuildingBlocks.nonEmpty) {
       val thread = threadBuildingBlocks.top.thread
       node match {
-        case c: VeyMontCondition[Pre] => c.condition.find{ case (threadRef,_) =>
-          threadRef.decl == thread
-        } match {
-          case Some((_,threadExpr)) => dispatch(threadExpr)
-          case _ => throw ParalliseVeyMontThreadsError(node, "Condition of if statement or while loop must contain an expression for every thread")
-        }
-        case m: MethodInvocation[Pre] => m.obj match {
-          case threadRef: DerefVeyMontThread[Pre] => m.rewrite(obj = dispatch(threadRef))
-          case _ => threadMethodSucc.get((thread, m.ref.decl)) match {
-            case Some(postMethod) => m.rewrite(obj = dispatch(m.obj), ref = postMethod.ref, m.args.map(dispatch))
-            case None => throw ParalliseVeyMontThreadsError(m, "No successor for this method found")
-          }
-        }
-        case d: Deref[Pre] => d.obj match {
-          case t: DerefVeyMontThread[Pre] =>
-            val threadField = threadBuildingBlocks.top.threadField
-            if(t.ref.decl == thread) {
-              d.rewrite(
-                obj = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), threadField.ref[InstanceField[Post]])(null)(d.o)
-              )
-            }
-            else rewriteDefault(node)
-
-        }
+        case c: VeyMontCondition[Pre] => paralleliseThreadCondition(node, thread, c)
+        case m: MethodInvocation[Pre] => updateThreadRefMethodInvoc(thread, m)
+        case d: Deref[Pre] => updateThreadRefInDeref(node, thread, d)
+        case t: DerefVeyMontThread[Pre] => updateThreadRefVeyMontDeref(node, thread, t)
         case _ => rewriteDefault(node)
       }
     } else rewriteDefault(node)
   }
 
+  private def updateThreadRefVeyMontDeref(node: Expr[Pre], thread: VeyMontThread[Pre], t: DerefVeyMontThread[Pre]) = {
+    if (t.ref.decl == thread) {
+      getThisVeyMontDeref(thread, t.o, threadBuildingBlocks.top.threadField)
+    } else rewriteDefault(node)
+  }
 
-    override def dispatch(st : Statement[Pre]) : Statement[Post] = {
+  private def updateThreadRefInDeref(node: Expr[Pre], thread: VeyMontThread[Pre], d: Deref[Pre]) = {
+    d.obj match {
+      case t: DerefVeyMontThread[Pre] =>
+        if (t.ref.decl == thread) {
+          d.rewrite(
+            obj = getThisVeyMontDeref(thread, d.o, threadBuildingBlocks.top.threadField)
+          )
+        }
+        else rewriteDefault(node)
+    }
+  }
+
+  private def updateThreadRefMethodInvoc(thread: VeyMontThread[Pre], m: MethodInvocation[Pre]) = {
+    m.obj match {
+      case threadRef: DerefVeyMontThread[Pre] => m.rewrite(obj = dispatch(threadRef))
+      case _ => threadMethodSucc.get((thread, m.ref.decl)) match {
+        case Some(postMethod) => m.rewrite(obj = dispatch(m.obj), ref = postMethod.ref, m.args.map(dispatch))
+        case None => throw ParalliseVeyMontThreadsError(m, "No successor for this method found")
+      }
+    }
+  }
+
+  private def paralleliseThreadCondition(node: Expr[Pre], thread: VeyMontThread[Pre], c: VeyMontCondition[Pre]) = {
+    c.condition.find { case (threadRef, _) =>
+      threadRef.decl == thread
+    } match {
+      case Some((_, threadExpr)) => dispatch(threadExpr)
+      case _ => throw ParalliseVeyMontThreadsError(node, "Condition of if statement or while loop must contain an expression for every thread")
+    }
+  }
+
+  private def getThisVeyMontDeref(thread: VeyMontThread[Pre], o: Origin, threadField: InstanceField[Rewritten[Pre]]) = {
+    Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), threadField.ref[InstanceField[Post]])(null)(o)
+  }
+
+  override def dispatch(st : Statement[Pre]) : Statement[Post] = {
       if (threadBuildingBlocks.nonEmpty) {
         val thread = threadBuildingBlocks.top.thread
         st match {
-          case v@VeyMontCommExpression(recv,sender,chanType,assign) =>
-            val channelField = threadBuildingBlocks.top.channelFields((v,v.o))
-            val channelClass = threadBuildingBlocks.top.channelClasses(chanType)
-            val thisChanField = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), channelField.ref[InstanceField[Post]])(null)(assign.o)
-            val assignment = assign.asInstanceOf[Assign[Pre]]
-            if (recv.decl == thread) {
-              val readMethod = findChannelClassMethod(v, channelClass, "readValue")
-              val assignValue = JavaInvocation(Some(thisChanField),Seq.empty, "readValue",Seq.empty, Seq.empty,Seq.empty)(null)(v.o)
-              assignValue.ref = Some(RefJavaMethod(readMethod))
-              Assign(dispatch(assignment.target),assignValue)(null)(v.o)
-            } else if(sender.decl == thread) {
-              val writeMethod = findChannelClassMethod(v, channelClass, "writeValue")
-              val writeInvoc = JavaInvocation(Some(thisChanField),Seq.empty,"writeValue",Seq(dispatch(assignment.value)),Seq.empty,Seq.empty)(null)(v.o)
-              writeInvoc.ref = Some(RefJavaMethod(writeMethod))
-              Eval(writeInvoc)(v.o)
-            }
-            else Skip()(assign.o)
+          case v: VeyMontCommExpression[Pre] =>
+            paralleliseVeyMontCommExpr(thread, v, createParComBlocks(thread, v))
           case v@VeyMontAssignExpression(threadRef, assign) =>
             if (threadRef.decl == thread)
               dispatch(assign)
-            else Skip()(assign.o)
-          case a: Assign[Pre] => rewriteDefault(st)
+            else Block(Seq.empty)(assign.o)
+          case a: Assign[Pre] => Assign(dispatch(a.target),dispatch(a.value))(a.blame)(a.o)
           case Branch(_) => rewriteDefault(st)
           case Loop(_, _, _, _, _) => rewriteDefault(st)
           case Scope(_, _) => rewriteDefault(st)
           case Block(_) => rewriteDefault(st)
-          case Eval(expr) => expr match {
-            case m: MethodInvocation[Pre] => m.obj match {
-              case _: ThisSeqProg[Pre] => Eval(dispatch(expr))(st.o)
-              case d: DerefVeyMontThread[Pre] => if(d.ref.decl == thread) Eval(dispatch(expr))(st.o) else Skip()(st.o)
-              case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
-            }
-            case _ => rewriteDefault(st)
-          }
-          case _: Assert[Pre] => Skip()(st.o)
+          case Eval(expr) => paralleliseMethodInvocation(st, thread, expr)
+          case _: Assert[Pre] => Block(Seq.empty)(st.o)
           case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
         }
       } else rewriteDefault(st)
     }
 
+  private def createParComBlocks(thread: VeyMontThread[Pre], v: VeyMontCommExpression[Pre]): ParallelCommExprBuildingBlocks[Pre] = {
+    val channelField = threadBuildingBlocks.top.channelFields((v, v.o))
+    val channelClass = threadBuildingBlocks.top.channelClasses(v.chanType)
+    val thisChanField = Deref(ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), channelField.ref[InstanceField[Post]])(null)(v.assign.o)
+    val assignment = v.assign.asInstanceOf[Assign[Pre]]
+    new ParallelCommExprBuildingBlocks(channelField, channelClass, thisChanField, assignment)
+  }
+
+  private def paralleliseMethodInvocation(st: Statement[Pre], thread: VeyMontThread[Pre], expr: Expr[Pre]): Statement[Post] = {
+    expr match {
+      case m: MethodInvocation[Pre] => m.obj match {
+        case _: ThisSeqProg[Pre] => Eval(m.rewrite(obj = ThisObject(threadClassSucc.ref[Post, Class[Post]](thread))(thread.o), ref = threadMethodSucc.ref((thread, m.ref.decl))))(st.o)
+        case d: DerefVeyMontThread[Pre] => if (d.ref.decl == thread) Eval(dispatch(expr))(st.o) else Block(Seq.empty)(st.o)
+        case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
+      }
+      case _ => throw ParalliseVeyMontThreadsError(st, "Statement not allowed in seq_program")
+    }
+  }
+
+  private def paralleliseVeyMontCommExpr(thread: VeyMontThread[Pre], v: VeyMontCommExpression[Pre], blocks: ParallelCommExprBuildingBlocks[Pre]): Statement[Post] = {
+    if (v.receiver.decl == thread) {
+      val readMethod = findChannelClassMethod(v, blocks.channelClass, "readValue")
+      val assignValue = JavaInvocation(Some(blocks.thisChanField), Seq.empty, "readValue", Seq.empty, Seq.empty, Seq.empty)(null)(v.o)
+      assignValue.ref = Some(RefJavaMethod(readMethod))
+      Assign(dispatch(blocks.assign.target), assignValue)(null)(v.o)
+    } else if (v.sender.decl == thread) {
+      val writeMethod = findChannelClassMethod(v, blocks.channelClass, "writeValue")
+      val writeInvoc = JavaInvocation(Some(blocks.thisChanField), Seq.empty, "writeValue", Seq(dispatch(blocks.assign.value)), Seq.empty, Seq.empty)(null)(v.o)
+      writeInvoc.ref = Some(RefJavaMethod(writeMethod))
+      Eval(writeInvoc)(v.o)
+    }
+    else Block(Seq.empty)(blocks.assign.o)
+  }
+
   private def findChannelClassMethod(v: VeyMontCommExpression[Pre], channelClass: JavaClass[Post], methodName: String): JavaMethod[Post] = {
     val method = channelClass.decls.find {
       case jm: JavaMethod[Post] => jm.name == methodName
diff --git a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
index 89140d8ec2..8e7cead537 100644
--- a/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
+++ b/src/rewrite/vct/rewrite/veymont/ThreadBuildingBlocks.scala
@@ -1,8 +1,7 @@
 package vct.rewrite.veymont
 
-import vct.col.ast.{ClassDeclaration, InstanceField, JavaClass, Statement, Type, VeyMontCommExpression, VeyMontThread}
+import vct.col.ast.{ClassDeclaration, InstanceField, JavaClass, Type, VeyMontCommExpression, VeyMontThread}
 import vct.col.origin.Origin
-import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewritten}
 
 class ThreadBuildingBlocks[Pre <: Generation](

From c102654f3d14dad4d1a1960e7f31482012cdf94e Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Wed, 12 Jul 2023 17:25:41 +0200
Subject: [PATCH 15/20] stuck at NoSuchElementException

---
 src/col/vct/col/ast/Node.scala                |  1 -
 .../vct/col/typerules/CoercingRewriter.scala  |  1 -
 .../veymont/ParalleliseVeyMontThreads.scala   | 71 +++++++++++--------
 3 files changed, 40 insertions(+), 33 deletions(-)

diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 9c066f1b7d..9d0d937320 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -189,7 +189,6 @@ final case class WandApply[G](res: Expr[G])(val blame: Blame[WandApplyFailed])(i
 final case class Havoc[G](loc: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with HavocImpl[G]
 final case class FramedProof[G](pre: Expr[G], body: Statement[G], post: Expr[G])(val blame: Blame[FramedProofFailure])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FramedProofImpl[G]
 final case class Extract[G](contractedStatement: Statement[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with ExtractImpl[G]
-final case class Skip[G]()(implicit val o: Origin) extends NormallyCompletingStatement[G]
 
 sealed trait ExceptionalStatement[G] extends Statement[G] with ExceptionalStatementImpl[G]
 final case class Eval[G](expr: Expr[G])(implicit val o: Origin) extends ExceptionalStatement[G] with EvalImpl[G]
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 99fd2b8945..508ff96ce1 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1574,7 +1574,6 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case ass @ SilverFieldAssign(obj, field, value) => SilverFieldAssign(ref(obj), field, coerce(value, field.decl.t))(ass.blame)
       case SilverLocalAssign(v, value) => SilverLocalAssign(v, coerce(value, v.decl.t))
       case SilverNewRef(v, fields) => SilverNewRef(v, fields)
-      case Skip() => Skip()
       case SpecIgnoreEnd() => SpecIgnoreEnd()
       case SpecIgnoreStart() => SpecIgnoreStart()
       case Switch(expr, body) => Switch(expr, body)
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 3e13008df4..a109e8adec 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,19 +1,14 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast
-import vct.col.ast.RewriteHelpers.{RewriteAssign, RewriteDeref, RewriteJavaClass, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
-import vct.col.origin.{Origin, PreferredNameOrigin}
-import vct.col.ref.Ref
+import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
+import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefJavaMethod
-import vct.col.rewrite.veymont.AddVeyMontAssignmentNodes.getDerefsFromExpr
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
-import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelClassOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
-
-import scala.collection.immutable.Seq
+import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
 
 object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   override def key: String = "ParalleliseVeyMontThreads"
@@ -36,7 +31,7 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
     override def shortPosition: String = thread.o.shortPosition
   }
 
-  case class ChannelClassOrigin(channelName: String, assign: Statement[_]) extends Origin {
+  case class ChannelFieldOrigin(channelName: String, assign: Statement[_]) extends Origin {
     override def preferredName: String = channelName
 
     override def context: String = assign.o.context
@@ -52,15 +47,13 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   private val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
   private val threadClassSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
   private val threadMethodSucc: SuccessionMap[(VeyMontThread[Pre],ClassDeclaration[Pre]),InstanceMethod[Post]] = SuccessionMap()
+  private val channelClassSucc: SuccessionMap[Type[Pre],JavaClass[Post]] = SuccessionMap()
+  private val channelClassName = "Channel"
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
-      case seqProg: VeyMontSeqProg[Pre] =>
-        val (channelClasses,channelFields) = extractChannelInfo(seqProg)
-        dispatchThreads(seqProg, channelClasses, channelFields)
-      case thread: VeyMontThread[Pre] => {
-        dispatchThread(thread)
-      }
+      case seqProg: VeyMontSeqProg[Pre] => dispatchThreads(seqProg)
+      case thread: VeyMontThread[Pre] => dispatchThread(thread)
       case other => rewriteDefault(other)
     }
   }
@@ -73,23 +66,28 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     } else rewriteDefault(thread)
   }
 
-  private def dispatchThreads(seqProg: VeyMontSeqProg[Pre], channelClasses: Map[Type[Pre], JavaClass[Post]], channelFields: Map[(VeyMontCommExpression[Pre], Origin), InstanceField[Post]]): Unit = {
+  private def dispatchThreads(seqProg: VeyMontSeqProg[Pre]): Unit = {
+    val (channelClasses,indexedChannelInfo) = extractChannelInfo(seqProg)
+    channelClasses.foreach{ case (t,c) =>
+      globalDeclarations.declare(c)
+      channelClassSucc.update(t,c)
+    }
     seqProg.threads.foreach(thread => {
       val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+      val channelFields = getChannelFields(thread, indexedChannelInfo, channelClasses)
       threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
         dispatch(thread)
       }
     })
   }
 
-  private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Map[(VeyMontCommExpression[Pre], Origin), InstanceField[Post]]) = {
+  private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = {
     val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
     val indexedChannelInfo: Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
       if (chanInfoSeq.size <= 1) chanInfoSeq
       else chanInfoSeq.zipWithIndex.map { case (chanInfo, index) => new ChannelInfo(chanInfo.comExpr, chanInfo.channelType, chanInfo.channelName + index) }).toSeq
     val channelClasses = generateChannelClasses(indexedChannelInfo)
-    val channelFields = getChannelFields(indexedChannelInfo, channelClasses)
-    (channelClasses, channelFields)
+    (channelClasses, indexedChannelInfo)
   }
 
   private def createThreadMethod(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre]) = {
@@ -101,13 +99,10 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   }
 
   private def createThreadClass(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre], threadMethods: Seq[ClassDeclaration[Post]]): Unit = {
-    val channelFieldsForThread = threadRes.channelFields.view.filterKeys {
-      case (comExpr,_) => comExpr.receiver.decl == thread || comExpr.sender.decl == thread
-    }.values.toSeq
     val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
     classDeclarations.scope {
       val threadClass = new Class[Post](
-        (threadRes.threadField +: channelFieldsForThread) ++ (threadRun +: threadMethods), Seq(), BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
+        (threadRes.threadField +: threadRes.channelFields.values.toSeq) ++ (threadRun +: threadMethods), Seq(), BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
       globalDeclarations.declare(threadClass)
       threadClassSucc.update(thread, threadClass)
     }
@@ -123,21 +118,30 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     case _ => throw ParalliseVeyMontThreadsError(thread, "RunMethod expected in seq_program")
   }
 
-  private def getChannelFields(channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[(VeyMontCommExpression[Pre],Origin),InstanceField[Post]] = {
-    channelInfo.map { chanInfo =>
-      val chanField = new InstanceField[Post](JavaTClass(channelClasses(chanInfo.channelType).ref,Seq.empty), Set.empty)(ChannelClassOrigin(chanInfo.channelName,chanInfo.comExpr.assign))
-      ((chanInfo.comExpr,chanInfo.comExpr.o), chanField) }.toMap
+  private def getChannelFields(thread: VeyMontThread[Pre], channelInfo: Seq[ChannelInfo[Pre]], channelClasses: Map[Type[Pre],JavaClass[Post]]): Map[(VeyMontCommExpression[Pre],Origin),InstanceField[Post]] = {
+    channelInfo
+      .filter( chanInfo => chanInfo.comExpr.receiver.decl == thread || chanInfo.comExpr.sender.decl == thread)
+      .map { chanInfo =>
+        val chanFieldOrigin = ChannelFieldOrigin(chanInfo.channelName,chanInfo.comExpr.assign)
+        val chanField = new InstanceField[Post](JavaTClass(channelClassSucc.ref(chanInfo.channelType),Seq.empty), Set.empty)(chanFieldOrigin)
+        ((chanInfo.comExpr, chanInfo.comExpr.o), chanField)
+      }.toMap
   }
 
+  private def getChannelClassName(channelType: Type[_]): String =
+    channelType.toString.capitalize + channelClassName
+
   private def generateChannelClasses(channelInfo: Seq[ChannelInfo[Pre]]) : Map[Type[Pre],JavaClass[Post]] = {
     val channelTypes = channelInfo.map(_.channelType).toSet
     channelTypes.map(channelType =>
       channelType -> {
         val chanClassPre = channelClass.asInstanceOf[JavaClass[Pre]]
         val rw = ChannelClassGenerator(channelType)
-        new RewriteJavaClass[Pre, Post](chanClassPre)(rw).rewrite(decls = classDeclarations.collect {
-          chanClassPre.decls.foreach(d => rw.dispatch(d))
-        }._1)
+        new RewriteJavaClass[Pre, Post](chanClassPre)(rw).rewrite(
+          name = getChannelClassName(channelType),
+          decls = classDeclarations.collect {
+            chanClassPre.decls.foreach(d => rw.dispatch(d))
+          }._1)
       }
     ).toMap
   }
@@ -152,6 +156,11 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         } else rewriteDefault(jnt)
       case _ => rewriteDefault(t)
     }
+
+    override def dispatch(decl: Declaration[Pre]): Unit = decl match {
+      case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType))) //TODO: deze rewrite verwijderd de constructor..
+      case other => rewriteDefault(other)
+    }
   }
 
   private def collectChannelsFromRun(seqProg: VeyMontSeqProg[Pre]) =

From f36c2ba2d4ee979f98c7fd87326c99f95f6710f4 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Thu, 13 Jul 2023 17:26:15 +0200
Subject: [PATCH 16/20] VeyMont produces output

---
 src/main/vct/main/modes/VeyMont.scala         |  2 +-
 src/main/vct/main/stages/CodeGeneration.scala | 67 +++++++++++++++++++
 src/main/vct/main/stages/Stages.scala         |  5 +-
 src/main/vct/main/stages/Transformation.scala |  9 ++-
 .../veymont/ParalleliseVeyMontThreads.scala   |  2 +-
 5 files changed, 76 insertions(+), 9 deletions(-)
 create mode 100644 src/main/vct/main/stages/CodeGeneration.scala

diff --git a/src/main/vct/main/modes/VeyMont.scala b/src/main/vct/main/modes/VeyMont.scala
index c9405ebe20..cb51f3a472 100644
--- a/src/main/vct/main/modes/VeyMont.scala
+++ b/src/main/vct/main/modes/VeyMont.scala
@@ -14,7 +14,7 @@ object VeyMont extends LazyLogging {
 
   def verifyWithOptions(options: Options, inputs: Seq[PathOrStd]) = {
     val collector = BlameCollector()
-    val stages = Stages.veymontOfOptions(options, ConstantBlameProvider(collector))
+    val stages = Stages.veymontTransformationOfOptions(options, ConstantBlameProvider(collector))
     logger.debug("Stages: " ++ stages.flatNames.map(_._1).mkString(", "))
     stages.run(inputs) match {
       case Left(value) => logger.error(value.text)
diff --git a/src/main/vct/main/stages/CodeGeneration.scala b/src/main/vct/main/stages/CodeGeneration.scala
new file mode 100644
index 0000000000..0e350061f2
--- /dev/null
+++ b/src/main/vct/main/stages/CodeGeneration.scala
@@ -0,0 +1,67 @@
+package vct.main.stages
+
+import hre.progress.Progress
+import hre.stages.Stage
+import vct.col.ast.{JavaClass, Node, Verification}
+import vct.col.print.Ctx
+import vct.col.rewrite.{Generation, PrettifyBlocks, RewriterBuilder}
+import vct.importer.Util
+import vct.main.stages.Transformation.writeOutFunctions
+import vct.options.Options
+import vct.options.types.{Backend, PathOrStd}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads
+
+object CodeGeneration {
+
+  private def writeOutFunctions(m: Map[String, PathOrStd]): Seq[(String, Verification[_ <: Generation] => Unit)] =
+    m.toSeq.map {
+      case (key, out) => (key, (program: Verification[_ <: Generation]) => out.write { writer =>
+        program.write(writer)(Ctx().namesIn(program))
+      })
+    }
+
+  def veymontGenerationOfOptions(options: Options): VeyMontGeneration =
+    options.backend match {
+      case Backend.Silicon | Backend.Carbon =>
+        VeyMontGeneration(
+          onBeforePassKey = writeOutFunctions(options.outputBeforePass),
+          onAfterPassKey = writeOutFunctions(options.outputAfterPass),
+          channelClass = Util.loadJavaClass(options.veymontChannel),
+        )
+    }
+}
+
+class CodeGeneration(val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)],
+                     val passes: Seq[RewriterBuilder]
+                       ) extends Stage[Verification[_ <: Generation], Verification[_ <: Generation]] {
+  override def friendlyName: String = "Generating VeyMont output"
+
+  override def progressWeight: Int = 1
+
+  override def run(input: Verification[_ <: Generation]): Verification[_ <: Generation] = {
+    var result: Verification[_ <: Generation] = input
+    Progress.foreach(passes, (pass: RewriterBuilder) => pass.key) { pass =>
+      onBeforePassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = pass().dispatch(result)
+
+      onAfterPassKey.foreach {
+        case (key, action) => if (pass.key == key) action(result)
+      }
+
+      result = PrettifyBlocks().dispatch(result)
+    }
+    result
+  }
+
+}
+
+case class VeyMontGeneration(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
+                             channelClass: JavaClass[_])
+  extends CodeGeneration(onBeforePassKey, onAfterPassKey, Seq(
+    ParalleliseVeyMontThreads.withArg(channelClass),
+  ))
diff --git a/src/main/vct/main/stages/Stages.scala b/src/main/vct/main/stages/Stages.scala
index cc7155ebda..2be2b1151a 100644
--- a/src/main/vct/main/stages/Stages.scala
+++ b/src/main/vct/main/stages/Stages.scala
@@ -58,10 +58,11 @@ case object Stages {
       .thenRun(ExpectedErrors.ofOptions(options))
   }
 
-  def veymontOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
+  def veymontTransformationOfOptions(options: Options, blameProvider: BlameProvider): Stages[Seq[Readable], Unit] = {
     Parsing.ofOptions(options, blameProvider)
       .thenRun(Resolution.ofOptions(options, blameProvider))
-      .thenRun(Transformation.veymontOfOptions(options))
+      .thenRun(Transformation.veymontTransformationOfOptions(options))
+      .thenRun(CodeGeneration.veymontGenerationOfOptions(options))
       .thenRun(Output.veymontOfOptions(options))
   }
 
diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index ad04613619..11131f15ef 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -65,13 +65,12 @@ object Transformation {
         )
     }
 
-  def veymontOfOptions(options: Options): Transformation =
+  def veymontTransformationOfOptions(options: Options): Transformation =
     options.backend match {
       case Backend.Silicon | Backend.Carbon =>
         VeyMontTransformation(
           onBeforePassKey = writeOutFunctions(options.outputBeforePass),
           onAfterPassKey = writeOutFunctions(options.outputAfterPass),
-          channelClass = Util.loadJavaClass(options.veymontChannel),
         )
     }
 }
@@ -289,12 +288,12 @@ case class SilverTransformation
   ))
 
 case class VeyMontTransformation(override val onBeforePassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
-                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
-                                 val channelClass: JavaClass[_])
+                                 override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil)
   extends Transformation(onBeforePassKey, onAfterPassKey, Seq(
     AddVeyMontAssignmentNodes,
     AddVeyMontConditionNodes,
     StructureCheck,
-    ParalleliseVeyMontThreads.withArg(channelClass),
   ))
 
+
+
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index a109e8adec..99158fa3ec 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -158,7 +158,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     }
 
     override def dispatch(decl: Declaration[Pre]): Unit = decl match {
-      case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType))) //TODO: deze rewrite verwijderd de constructor..
+      case jc: JavaConstructor[Pre] => classDeclarations.declare(jc.rewrite(name = getChannelClassName(channelType)))
       case other => rewriteDefault(other)
     }
   }

From 58664396d62b8fb1dc9e84f020412dd0e4a7c4ae Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Mon, 17 Jul 2023 19:21:37 +0200
Subject: [PATCH 17/20] A reference to the successor of this declaration was
 made, but it has no successor.

---
 src/col/vct/col/ast/Node.scala                |   3 +-
 src/col/vct/col/ast/lang/JavaFieldsImpl.scala |   2 +-
 .../ast/lang/JavaLocalDeclarationImpl.scala   |   2 +-
 src/col/vct/col/ast/lang/JavaMethodImpl.scala |   2 +-
 src/col/vct/col/ast/lang/JavaParamImpl.scala  |   9 ++
 src/col/vct/col/ast/type/TUnionImpl.scala     |   2 +
 .../col/ast/type/TVeyMontChannelImpl.scala    |   9 ++
 .../veymont/ParalleliseVeyMontThreads.scala   | 127 ++++++++++++++++--
 8 files changed, 139 insertions(+), 17 deletions(-)
 create mode 100644 src/col/vct/col/ast/lang/JavaParamImpl.scala
 create mode 100644 src/col/vct/col/ast/type/TVeyMontChannelImpl.scala

diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 9d0d937320..1d000bf8b5 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -141,6 +141,7 @@ final case class TAnyClass[G]()(implicit val o: Origin = DiagnosticOrigin) exten
 final case class TAxiomatic[G](adt: Ref[G, AxiomaticDataType[G]], args: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TAxiomaticImpl[G]
 final case class TEnum[G](enum: Ref[G, Enum[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G]
 final case class TProverType[G](ref: Ref[G, ProverType[G]])(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TProverTypeImpl[G]
+final case class TVeyMontChannel[G](channelType: String)(implicit val o: Origin = DiagnosticOrigin) extends DeclaredType[G] with TVeyMontChannelImpl[G]
 
 sealed trait ParRegion[G] extends NodeFamily[G] with ParRegionImpl[G]
 final case class ParParallel[G](regions: Seq[ParRegion[G]])(val blame: Blame[ParPreconditionFailed])(implicit val o: Origin) extends ParRegion[G] with ParParallelImpl[G]
@@ -994,7 +995,7 @@ sealed trait JavaClassDeclaration[G] extends ClassDeclaration[G] with JavaClassD
 final class JavaSharedInitialization[G](val isStatic: Boolean, val initialization: Statement[G])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaSharedInitializationImpl[G]
 final class JavaFields[G](val modifiers: Seq[JavaModifier[G]], val t: Type[G], val decls: Seq[JavaVariableDeclaration[G]])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaFieldsImpl[G]
 final class JavaConstructor[G](val modifiers: Seq[JavaModifier[G]], val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Statement[G], val contract: ApplicableContract[G])(val blame: Blame[ConstructorFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaConstructorImpl[G]
-final class JavaParam[G](val modifiers: Seq[JavaModifier[G]], val name: String, val t: Type[G])(implicit val o: Origin) extends Declaration[G]
+final class JavaParam[G](val modifiers: Seq[JavaModifier[G]], val name: String, val t: Type[G])(implicit val o: Origin) extends Declaration[G] with JavaParamImpl[G]
 
 final class JavaMethod[G](val modifiers: Seq[JavaModifier[G]], val returnType: Type[G], val dims: Int, val name: String, val parameters: Seq[JavaParam[G]], val typeParameters: Seq[Variable[G]], val signals: Seq[Type[G]], val body: Option[Statement[G]], val contract: ApplicableContract[G])(val blame: Blame[CallableFailure])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaMethodImpl[G]
 final class JavaAnnotationMethod[G](val returnType: Type[G], val name: String, val default: Option[Expr[G]])(implicit val o: Origin) extends JavaClassDeclaration[G] with JavaAnnotationMethodImpl[G]
diff --git a/src/col/vct/col/ast/lang/JavaFieldsImpl.scala b/src/col/vct/col/ast/lang/JavaFieldsImpl.scala
index b5cce4b2cb..9749895420 100644
--- a/src/col/vct/col/ast/lang/JavaFieldsImpl.scala
+++ b/src/col/vct/col/ast/lang/JavaFieldsImpl.scala
@@ -7,5 +7,5 @@ trait JavaFieldsImpl[G] { this: JavaFields[G] =>
   override def isStatic = modifiers.contains(JavaStatic[G]())
 
   override def layout(implicit ctx: Ctx): Doc =
-    Doc.lspread(modifiers) <> t <+> Doc.spread(decls) <> ";"
+    Doc.rspread(modifiers) <> t <+> Doc.spread(decls) <> ";"
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/JavaLocalDeclarationImpl.scala b/src/col/vct/col/ast/lang/JavaLocalDeclarationImpl.scala
index ae4b1c024b..c2c1d5668a 100644
--- a/src/col/vct/col/ast/lang/JavaLocalDeclarationImpl.scala
+++ b/src/col/vct/col/ast/lang/JavaLocalDeclarationImpl.scala
@@ -5,5 +5,5 @@ import vct.col.print.{Ctx, Doc, Group}
 
 trait JavaLocalDeclarationImpl[G] { this: JavaLocalDeclaration[G] =>
   override def layout(implicit ctx: Ctx): Doc =
-    Group(Doc.lspread(modifiers) <> t <+> Doc.args(decls))
+    Group(Doc.rspread(modifiers) <> t <+> Doc.args(decls))
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/lang/JavaMethodImpl.scala b/src/col/vct/col/ast/lang/JavaMethodImpl.scala
index ce9b1a7fc9..9a3c00bb0d 100644
--- a/src/col/vct/col/ast/lang/JavaMethodImpl.scala
+++ b/src/col/vct/col/ast/lang/JavaMethodImpl.scala
@@ -12,7 +12,7 @@ trait JavaMethodImpl[G] extends Declarator[G] { this: JavaMethod[G] =>
     Doc.stack(Seq(
       contract,
       Group(Group(Group(
-        Doc.lspread(modifiers) <>
+        Doc.rspread(modifiers) <>
         (if(typeParameters.isEmpty) Empty else Text("<") <> Doc.args(typeParameters) <> ">" <+> Empty) <>
         returnType <+> name <> "[]".repeat(dims)) <> "(" <> Doc.args(parameters) <> ")") <>
         (if(signals.isEmpty) Empty else Empty <>> Group(Text("throws") <+> Doc.args(signals)))
diff --git a/src/col/vct/col/ast/lang/JavaParamImpl.scala b/src/col/vct/col/ast/lang/JavaParamImpl.scala
new file mode 100644
index 0000000000..9f3b2e1b99
--- /dev/null
+++ b/src/col/vct/col/ast/lang/JavaParamImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.lang
+
+import vct.col.ast.JavaParam
+import vct.col.print.{Ctx, Doc, Text}
+
+trait JavaParamImpl[G] { this: JavaParam[G] =>
+  override def layout(implicit ctx: Ctx): Doc = Text(t + " " + name)
+
+}
diff --git a/src/col/vct/col/ast/type/TUnionImpl.scala b/src/col/vct/col/ast/type/TUnionImpl.scala
index c598defaa8..af0f33e3e1 100644
--- a/src/col/vct/col/ast/type/TUnionImpl.scala
+++ b/src/col/vct/col/ast/type/TUnionImpl.scala
@@ -1,7 +1,9 @@
 package vct.col.ast.`type`
 
 import vct.col.ast.TUnion
+import vct.col.print.{Ctx, Doc}
 
 trait TUnionImpl[G] { this: TUnion[G] =>
+  override def layout(implicit ctx: Ctx): Doc =  Doc.spread(types)
 
 }
\ No newline at end of file
diff --git a/src/col/vct/col/ast/type/TVeyMontChannelImpl.scala b/src/col/vct/col/ast/type/TVeyMontChannelImpl.scala
new file mode 100644
index 0000000000..7c73695267
--- /dev/null
+++ b/src/col/vct/col/ast/type/TVeyMontChannelImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.`type`
+
+import vct.col.ast.TVeyMontChannel
+import vct.col.print.{Ctx, Doc, Text}
+
+trait TVeyMontChannelImpl[G] { this: TVeyMontChannel[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Text(this.channelType)
+}
\ No newline at end of file
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index 99158fa3ec..ebe3107304 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,20 +1,33 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.RewriteHelpers.{RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
-import vct.col.ast.{Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaMethod, JavaNamedType, JavaTClass, Local, Loop, MethodInvocation, Node, Program, RunMethod, Scope, Statement, TClass, ThisObject, ThisSeqProg, Type, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.RewriteHelpers.{RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
+import vct.col.ast.{ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefJavaMethod
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
-import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin, getChannelClassName, getThreadClassName, getVarName}
+
+import java.lang
 
 object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   override def key: String = "ParalleliseVeyMontThreads"
 
   override def desc: String = "Generate classes for VeyMont threads in parallel program"
 
+  private val channelClassName = "Channel"
+  private val threadClassName = "Thread"
+
+  def getChannelClassName(channelType: Type[_]): String =
+    channelType.toString.capitalize + channelClassName
+
+  def getThreadClassName(thread: VeyMontThread[_]) : String =
+    thread.o.preferredName.capitalize + threadClassName
+
+  def getVarName(v: Variable[_]) = v.o.preferredName
+
   case class ParalliseVeyMontThreadsError(node : Node[_], msg: String) extends UserError {
     override def code: String = "ParalleliseVeyMontThreadsError"
 
@@ -22,7 +35,7 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
   }
 
   case class ThreadClassOrigin(thread: VeyMontThread[_]) extends Origin {
-    override def preferredName: String = thread.o.preferredName.toUpperCase() + "Thread"
+    override def preferredName: String = getThreadClassName(thread)
 
     override def context: String = thread.o.context
 
@@ -47,11 +60,13 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   private val threadBuildingBlocks: ScopedStack[ThreadBuildingBlocks[Pre]] = ScopedStack()
   private val threadClassSucc: SuccessionMap[VeyMontThread[Pre],Class[Post]] = SuccessionMap()
   private val threadMethodSucc: SuccessionMap[(VeyMontThread[Pre],ClassDeclaration[Pre]),InstanceMethod[Post]] = SuccessionMap()
-  private val channelClassSucc: SuccessionMap[Type[Pre],JavaClass[Post]] = SuccessionMap()
-  private val channelClassName = "Channel"
+  private val givenClassSucc: SuccessionMap[Type[Pre],Class[Post]] = SuccessionMap()
+  private val givenClassConstrSucc: SuccessionMap[Type[Pre],Procedure[Pre]] = SuccessionMap()
 
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
+      case p: Procedure[Pre] => givenClassConstrSucc.update(p.returnType,p)
+      case c : Class[Pre] => globalDeclarations.declare(dispatchGivenClass(c))
       case seqProg: VeyMontSeqProg[Pre] => dispatchThreads(seqProg)
       case thread: VeyMontThread[Pre] => dispatchThread(thread)
       case other => rewriteDefault(other)
@@ -70,10 +85,9 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     val (channelClasses,indexedChannelInfo) = extractChannelInfo(seqProg)
     channelClasses.foreach{ case (t,c) =>
       globalDeclarations.declare(c)
-      channelClassSucc.update(t,c)
     }
     seqProg.threads.foreach(thread => {
-      val threadField = new InstanceField[Post](dispatch(thread.threadType), Set.empty)(thread.o)
+      val threadField = new InstanceField[Post](TClass(givenClassSucc.ref(thread.threadType)), Set.empty)(thread.o)
       val channelFields = getChannelFields(thread, indexedChannelInfo, channelClasses)
       threadBuildingBlocks.having(new ThreadBuildingBlocks(seqProg.runMethod, seqProg.methods, channelFields, channelClasses, thread, threadField)) {
         dispatch(thread)
@@ -81,6 +95,65 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     })
   }
 
+  private def dispatchGivenClass(c: Class[Pre]): Class[Post] = {
+    val rw = GivenClassRewriter()
+    val gc = new RewriteClass[Pre, Post](c)(rw).rewrite(
+      declarations = classDeclarations.collect {
+        (givenClassConstrSucc.get(TClass(c.ref)).get +: c.declarations).foreach(d => rw.dispatch(d))
+      }._1)
+    givenClassSucc.update(TClass(c.ref),gc)
+    gc
+  }
+
+  case class GivenClassRewriter() extends Rewriter[Pre] {
+    override val allScopes = outer.allScopes
+
+    val rewritingConstr: ScopedStack[(Seq[Variable[Pre]],TClass[Pre])] = ScopedStack()
+
+    override def dispatch(decl: Declaration[Pre]): Unit = decl match {
+      case p: Procedure[Pre] => p.returnType match {
+        case tc: TClass[Pre] => rewritingConstr.having(p.args,tc){ classDeclarations.declare(createClassConstructor(p)) };
+        case _ => ??? //("This procedure is expected to have a class as return type");
+      }
+      case other => rewriteDefault(other)
+    }
+
+    def createClassConstructor(p: Procedure[Pre]): JavaConstructor[Post] =
+      new JavaConstructor[Post](Seq(JavaPublic[Post]()(p.o)),
+        rewritingConstr.top._2.cls.decl.o.preferredName,
+        p.args.map(createJavaParam),
+        variables.dispatch(p.typeArgs),
+        Seq.empty, dispatch(p.body.get),
+        dispatch(p.contract))(null)(p.o)
+
+    def createJavaParam(v: Variable[Pre]): JavaParam[Post] =
+      new JavaParam[Post](Seq.empty, getVarName(v), dispatch(v.t))(v.o)
+
+    override def dispatch(e: Expr[Pre]): Expr[Post] = e match {
+      case l: Local[Pre] =>
+        if(rewritingConstr.nonEmpty && rewritingConstr.top._1.contains(l.ref.decl))
+          JavaLocal[Post](getVarName(l.ref.decl))(null)(e.o)
+        else rewriteDefault(l)
+      case no: NewObject[Pre] =>
+        val newClassType = TClass(no.cls)
+        if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == newClassType)
+          NewObject(givenClassSucc.ref[Post,Class[Post]](newClassType))(no.o)
+        else rewriteDefault(no)
+      case t: ThisObject[Pre] =>
+        val thisClassType = TClass(t.cls)
+        if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == thisClassType)
+          ThisObject(givenClassSucc.ref[Post,Class[Post]](thisClassType))(t.o)
+        else rewriteDefault(t)
+      case other => rewriteDefault(other)
+    }
+
+    override def dispatch(t: Type[Pre]): Type[Post] = {
+      if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == t)
+        TClass(givenClassSucc.ref(t))
+      else rewriteDefault(t)
+    }
+  }
+
   private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = {
     val channelInfo = collectChannelsFromRun(seqProg) ++ collectChannelsFromMethods(seqProg)
     val indexedChannelInfo: Seq[ChannelInfo[Pre]] = channelInfo.groupBy(_.channelName).values.flatMap(chanInfoSeq =>
@@ -99,15 +172,46 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   }
 
   private def createThreadClass(thread: VeyMontThread[Pre], threadRes: ThreadBuildingBlocks[Pre], threadMethods: Seq[ClassDeclaration[Post]]): Unit = {
+    val threadConstr = createThreadClassConstructor(thread,threadRes.threadField)
     val threadRun = getThreadRunFromDecl(thread, threadRes.runMethod)
     classDeclarations.scope {
       val threadClass = new Class[Post](
-        (threadRes.threadField +: threadRes.channelFields.values.toSeq) ++ (threadRun +: threadMethods), Seq(), BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
+        (threadRes.threadField +: threadRes.channelFields.values.toSeq) ++ (threadConstr +: threadRun +: threadMethods), Seq(), BooleanValue(true)(thread.o))(ThreadClassOrigin(thread))
       globalDeclarations.declare(threadClass)
       threadClassSucc.update(thread, threadClass)
     }
   }
 
+  private def createThreadClassConstructor(thread: VeyMontThread[Pre], threadField: InstanceField[Post]): JavaConstructor[Post] = {
+    val threadConstrArgBlocks = thread.args.map{
+      case l: Local[Pre] => (l.ref.decl.o.preferredName,dispatch(l.t))
+      case other => throw ParalliseVeyMontThreadsError(other,"This node is expected to be an argument of seq_prog, and have type Local")
+    }
+    val threadConstrArgs: Seq[JavaParam[Post]] =
+      threadConstrArgBlocks.map{ case (a,t) => new JavaParam[Post](Seq.empty, a, t)(ThreadClassOrigin(thread)) }
+    val passedArgs = threadConstrArgs.map(a => JavaLocal[Post](a.name)(null)(ThreadClassOrigin(thread)))
+    val ThreadTypeName = thread.threadType match {
+      case tc: TClass[Pre] => tc.cls.decl.o.preferredName
+      case _ => throw ParalliseVeyMontThreadsError(thread.threadType,"This type is expected to be a class")
+    }
+    val threadConstrBody = {
+      Assign(getThisVeyMontDeref(thread,ThreadClassOrigin(thread),threadField),
+      JavaInvocation[Post](None, Seq.empty, "new " + ThreadTypeName, passedArgs, Seq.empty, Seq.empty)(null)(ThreadClassOrigin(thread)))(null)(ThreadClassOrigin(thread))
+    }
+    val threadConstrContract = new ApplicableContract[Post](
+      UnitAccountedPredicate[Post](BooleanValue(true)(ThreadClassOrigin(thread)))(ThreadClassOrigin(thread)),
+      UnitAccountedPredicate[Post](BooleanValue(true)(ThreadClassOrigin(thread)))(ThreadClassOrigin(thread)),
+      BooleanValue(true)(ThreadClassOrigin(thread)),
+      Seq.empty, Seq.empty, Seq.empty, None)(null)(ThreadClassOrigin(thread))
+    new JavaConstructor[Post](
+      Seq(JavaPublic[Post]()(ThreadClassOrigin(thread))),
+      getThreadClassName(thread),
+      threadConstrArgs,
+      Seq.empty, Seq.empty,
+      threadConstrBody,
+      threadConstrContract)(ThreadClassOrigin(thread))(ThreadClassOrigin(thread))
+  }
+
   private def getThreadMethodFromDecl(thread: VeyMontThread[Pre])(decl: ClassDeclaration[Pre]): InstanceMethod[Post]  = decl match {
     case m: InstanceMethod[Pre] => getThreadMethod(m)
     case _ => throw ParalliseVeyMontThreadsError(thread, "Methods of seq_program need to be of type InstanceMethod")
@@ -123,14 +227,11 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
       .filter( chanInfo => chanInfo.comExpr.receiver.decl == thread || chanInfo.comExpr.sender.decl == thread)
       .map { chanInfo =>
         val chanFieldOrigin = ChannelFieldOrigin(chanInfo.channelName,chanInfo.comExpr.assign)
-        val chanField = new InstanceField[Post](JavaTClass(channelClassSucc.ref(chanInfo.channelType),Seq.empty), Set.empty)(chanFieldOrigin)
+        val chanField = new InstanceField[Post](TVeyMontChannel(getChannelClassName(chanInfo.channelType)), Set.empty)(chanFieldOrigin)
         ((chanInfo.comExpr, chanInfo.comExpr.o), chanField)
       }.toMap
   }
 
-  private def getChannelClassName(channelType: Type[_]): String =
-    channelType.toString.capitalize + channelClassName
-
   private def generateChannelClasses(channelInfo: Seq[ChannelInfo[Pre]]) : Map[Type[Pre],JavaClass[Post]] = {
     val channelTypes = channelInfo.map(_.channelType).toSet
     channelTypes.map(channelType =>

From 308204b4e6aeb15eaa3571416cb7daf119f61e88 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Mon, 17 Jul 2023 22:44:19 +0200
Subject: [PATCH 18/20] rewriting constructor to original format

---
 .../veymont/ParalleliseVeyMontThreads.scala   | 39 ++++++++++---------
 1 file changed, 21 insertions(+), 18 deletions(-)

diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index ebe3107304..c01acdae6e 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -1,11 +1,11 @@
 package vct.rewrite.veymont
 
 import hre.util.ScopedStack
-import vct.col.ast.RewriteHelpers.{RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
-import vct.col.ast.{ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.RewriteHelpers.{RewriteApplicableContract, RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
+import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefJavaMethod
-import vct.col.rewrite.{Generation, Rewriter, RewriterBuilderArg, Rewritten}
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
 import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin, getChannelClassName, getThreadClassName, getVarName}
@@ -123,8 +123,15 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         rewritingConstr.top._2.cls.decl.o.preferredName,
         p.args.map(createJavaParam),
         variables.dispatch(p.typeArgs),
-        Seq.empty, dispatch(p.body.get),
-        dispatch(p.contract))(null)(p.o)
+        Seq.empty,
+        p.body match {
+          case Some(s: Scope[Pre]) => s.body match {
+            case b: Block[Pre] => dispatch(Block(b.statements.tail.dropRight(1))(p.o))
+            case other => dispatch(other)
+          }
+          case None => Block(Seq.empty)(p.o)
+        },
+        p.contract.rewrite(ensures = UnitAccountedPredicate[Post](BooleanValue(true)(p.o))(p.o)))(null)(p.o)
 
     def createJavaParam(v: Variable[Pre]): JavaParam[Post] =
       new JavaParam[Post](Seq.empty, getVarName(v), dispatch(v.t))(v.o)
@@ -134,24 +141,20 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         if(rewritingConstr.nonEmpty && rewritingConstr.top._1.contains(l.ref.decl))
           JavaLocal[Post](getVarName(l.ref.decl))(null)(e.o)
         else rewriteDefault(l)
-      case no: NewObject[Pre] =>
-        val newClassType = TClass(no.cls)
-        if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == newClassType)
-          NewObject(givenClassSucc.ref[Post,Class[Post]](newClassType))(no.o)
-        else rewriteDefault(no)
       case t: ThisObject[Pre] =>
         val thisClassType = TClass(t.cls)
         if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == thisClassType)
           ThisObject(givenClassSucc.ref[Post,Class[Post]](thisClassType))(t.o)
         else rewriteDefault(t)
+      case d: Deref[Pre] =>
+        if(rewritingConstr.nonEmpty)
+          d.obj match {
+            case _: Local[Pre] => d.rewrite(obj = ThisObject(givenClassSucc.ref[Post,Class[Post]](rewritingConstr.top._2))(d.o))
+            case other => rewriteDefault(other)
+          }
+        else rewriteDefault(d)
       case other => rewriteDefault(other)
     }
-
-    override def dispatch(t: Type[Pre]): Type[Post] = {
-      if(rewritingConstr.nonEmpty && rewritingConstr.top._2 == t)
-        TClass(givenClassSucc.ref(t))
-      else rewriteDefault(t)
-    }
   }
 
   private def extractChannelInfo(seqProg: VeyMontSeqProg[Pre]): (Map[Type[Pre], JavaClass[Post]], Seq[ChannelInfo[Pre]]) = {
@@ -190,13 +193,13 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     val threadConstrArgs: Seq[JavaParam[Post]] =
       threadConstrArgBlocks.map{ case (a,t) => new JavaParam[Post](Seq.empty, a, t)(ThreadClassOrigin(thread)) }
     val passedArgs = threadConstrArgs.map(a => JavaLocal[Post](a.name)(null)(ThreadClassOrigin(thread)))
-    val ThreadTypeName = thread.threadType match {
+    val threadTypeName = thread.threadType match { //TODO: replace by using givenClassSucc
       case tc: TClass[Pre] => tc.cls.decl.o.preferredName
       case _ => throw ParalliseVeyMontThreadsError(thread.threadType,"This type is expected to be a class")
     }
     val threadConstrBody = {
       Assign(getThisVeyMontDeref(thread,ThreadClassOrigin(thread),threadField),
-      JavaInvocation[Post](None, Seq.empty, "new " + ThreadTypeName, passedArgs, Seq.empty, Seq.empty)(null)(ThreadClassOrigin(thread)))(null)(ThreadClassOrigin(thread))
+      JavaInvocation[Post](None, Seq.empty, "new " + threadTypeName, passedArgs, Seq.empty, Seq.empty)(null)(ThreadClassOrigin(thread)))(null)(ThreadClassOrigin(thread))
     }
     val threadConstrContract = new ApplicableContract[Post](
       UnitAccountedPredicate[Post](BooleanValue(true)(ThreadClassOrigin(thread)))(ThreadClassOrigin(thread)),

From 0a16fa69249f0d44204781e3fb03298aaa13326f Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Tue, 18 Jul 2023 13:13:00 +0200
Subject: [PATCH 19/20] compiling Java code

---
 .../veymont-seq-progs/veymont-swap.pvl        |  2 +-
 .../veymont/ParalleliseVeyMontThreads.scala   | 27 ++++++++++++++-----
 .../vct/rewrite/veymont/StructureCheck.scala  |  2 ++
 3 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/examples/technical/veymont-seq-progs/veymont-swap.pvl b/examples/technical/veymont-seq-progs/veymont-swap.pvl
index 471c083458..e39a0abd21 100644
--- a/examples/technical/veymont-seq-progs/veymont-swap.pvl
+++ b/examples/technical/veymont-seq-progs/veymont-swap.pvl
@@ -22,7 +22,7 @@ seq_program SeqProgram(int x, int y) {
    thread s1 = Storage(x);
    thread s2 = Storage(y);
 
-  int num() {}
+  //int num() {}
   
   void foo() {
      s1.temp = 7;
diff --git a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
index c01acdae6e..3d98b04c76 100644
--- a/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
+++ b/src/rewrite/vct/rewrite/veymont/ParalleliseVeyMontThreads.scala
@@ -2,13 +2,13 @@ package vct.rewrite.veymont
 
 import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.{RewriteApplicableContract, RewriteClass, RewriteDeref, RewriteJavaClass, RewriteJavaConstructor, RewriteMethodInvocation}
-import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
+import vct.col.ast.{AbstractRewriter, ApplicableContract, Assert, Assign, Block, BooleanValue, Branch, Class, ClassDeclaration, Declaration, Deref, DerefVeyMontThread, Eval, Expr, InstanceField, InstanceMethod, JavaClass, JavaConstructor, JavaInvocation, JavaLocal, JavaMethod, JavaNamedType, JavaParam, JavaPublic, JavaTClass, Local, Loop, MethodInvocation, NewObject, Node, Procedure, Program, RunMethod, Scope, Statement, TClass, TVeyMontChannel, TVoid, ThisObject, ThisSeqProg, Type, UnitAccountedPredicate, Variable, VeyMontAssignExpression, VeyMontCommExpression, VeyMontCondition, VeyMontSeqProg, VeyMontThread}
 import vct.col.origin.Origin
 import vct.col.resolve.ctx.RefJavaMethod
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, RewriterBuilderArg, Rewritten}
 import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
-import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, ThreadClassOrigin, getChannelClassName, getThreadClassName, getVarName}
+import vct.rewrite.veymont.ParalleliseVeyMontThreads.{ChannelFieldOrigin, ParalliseVeyMontThreadsError, RunMethodOrigin, ThreadClassOrigin, getChannelClassName, getThreadClassName, getVarName}
 
 import java.lang
 
@@ -53,6 +53,16 @@ object ParalleliseVeyMontThreads extends RewriterBuilderArg[JavaClass[_]] {
 
     override def shortPosition: String = assign.o.shortPosition
   }
+
+  case class RunMethodOrigin(runMethod: RunMethod[_]) extends Origin {
+    override def preferredName: String = "run"
+
+    override def context: String = runMethod.o.context
+
+    override def inlineContext: String = runMethod.o.inlineContext
+
+    override def shortPosition: String = runMethod.o.shortPosition
+  }
 }
 
 case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[_]) extends Rewriter[Pre] { outer =>
@@ -66,7 +76,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
   override def dispatch(decl : Declaration[Pre]) : Unit = {
     decl match {
       case p: Procedure[Pre] => givenClassConstrSucc.update(p.returnType,p)
-      case c : Class[Pre] => globalDeclarations.declare(dispatchGivenClass(c))
+      case c : Class[Pre] => globalDeclarations.succeed(c, dispatchGivenClass(c))
       case seqProg: VeyMontSeqProg[Pre] => dispatchThreads(seqProg)
       case thread: VeyMontThread[Pre] => dispatchThread(thread)
       case other => rewriteDefault(other)
@@ -220,7 +230,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
     case _ => throw ParalliseVeyMontThreadsError(thread, "Methods of seq_program need to be of type InstanceMethod")
   }
 
-  private def getThreadRunFromDecl(thread: VeyMontThread[Pre], decl: ClassDeclaration[Pre]): RunMethod[Post] = decl match {
+  private def getThreadRunFromDecl(thread: VeyMontThread[Pre], decl: ClassDeclaration[Pre]): InstanceMethod[Post] = decl match {
     case m: RunMethod[Pre] => getThreadRunMethod(m)
     case _ => throw ParalliseVeyMontThreadsError(thread, "RunMethod expected in seq_program")
   }
@@ -243,6 +253,7 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         val rw = ChannelClassGenerator(channelType)
         new RewriteJavaClass[Pre, Post](chanClassPre)(rw).rewrite(
           name = getChannelClassName(channelType),
+          modifiers = Seq.empty,
           decls = classDeclarations.collect {
             chanClassPre.decls.foreach(d => rw.dispatch(d))
           }._1)
@@ -302,10 +313,12 @@ case class ParalleliseVeyMontThreads[Pre <: Generation](channelClass: JavaClass[
         dispatch(method.contract))(method.blame)(method.o)
   }
 
-  private def getThreadRunMethod(run: RunMethod[Pre]): RunMethod[Post] = {
-    new RunMethod[Post](
+  private def getThreadRunMethod(run: RunMethod[Pre]): InstanceMethod[Post] = {
+    new InstanceMethod[Post](
+      TVoid[Post](),
+      Seq.empty,Seq.empty,Seq.empty,
       run.body.map(dispatch),
-      dispatch(run.contract))(run.blame)(run.o)
+      dispatch(run.contract))(run.blame)(RunMethodOrigin(run))
   }
 
   override def dispatch(node: Expr[Pre]): Expr[Post] = {
diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
index 8af88c94f6..28380a2822 100644
--- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
+++ b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala
@@ -33,6 +33,8 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
       case m: InstanceMethod[Pre] =>
         if (inSeqProg.nonEmpty && m.args.nonEmpty)
           throw VeyMontStructCheckError(m, "Methods in seq_program cannot have any arguments!")
+        else if(inSeqProg.nonEmpty && m.returnType != TVoid[Pre]())
+          throw VeyMontStructCheckError(m, "Methods in seq_program cannot have a non-void return type!")
         else rewriteDefault(decl)
       case r: RunMethod[Pre] =>
         if(r.body.isEmpty)

From 07bd995d1db0036d09458a37b60bfdf7da32d1b2 Mon Sep 17 00:00:00 2001
From: Petra van den Bos <p.vandenbos@utwente.nl>
Date: Thu, 20 Jul 2023 14:17:25 +0200
Subject: [PATCH 20/20] layout fixes

---
 src/col/vct/col/ast/lang/JavaParamImpl.scala | 2 +-
 src/col/vct/col/ast/type/TUnionImpl.scala    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/col/vct/col/ast/lang/JavaParamImpl.scala b/src/col/vct/col/ast/lang/JavaParamImpl.scala
index 9f3b2e1b99..0bbc63523b 100644
--- a/src/col/vct/col/ast/lang/JavaParamImpl.scala
+++ b/src/col/vct/col/ast/lang/JavaParamImpl.scala
@@ -4,6 +4,6 @@ import vct.col.ast.JavaParam
 import vct.col.print.{Ctx, Doc, Text}
 
 trait JavaParamImpl[G] { this: JavaParam[G] =>
-  override def layout(implicit ctx: Ctx): Doc = Text(t + " " + name)
+  override def layout(implicit ctx: Ctx): Doc = t.show <+> name
 
 }
diff --git a/src/col/vct/col/ast/type/TUnionImpl.scala b/src/col/vct/col/ast/type/TUnionImpl.scala
index af0f33e3e1..6aabe6796f 100644
--- a/src/col/vct/col/ast/type/TUnionImpl.scala
+++ b/src/col/vct/col/ast/type/TUnionImpl.scala
@@ -4,6 +4,6 @@ import vct.col.ast.TUnion
 import vct.col.print.{Ctx, Doc}
 
 trait TUnionImpl[G] { this: TUnion[G] =>
-  override def layout(implicit ctx: Ctx): Doc =  Doc.spread(types)
+  override def layout(implicit ctx: Ctx): Doc =  Doc.fold(types)(_ <+> "|" <+> _)
 
 }
\ No newline at end of file