diff --git a/src/common/configuration.k b/src/common/configuration.k
new file mode 100644
index 00000000..e257e786
--- /dev/null
+++ b/src/common/configuration.k
@@ -0,0 +1,341 @@
+module CONFIGURATION
+    imports CORE-SORTS
+    imports CORE-FUNCTIONS
+
+configuration
+    <T>
+      //Configuration part 1: threads
+      <threads color="GreenYellow">
+        <thread multiplicity="*" color="GreenYellow">
+          <k color="Green"> .K </k>
+
+          <stack color="Green"> .List </stack>
+
+          /*The execution context of the current method - local names environment, return type,
+            context type and current object.*/
+          <methodContext color="Orange">
+
+            //The map from local vars to their location in the store. Also includes outer local vars, for local classes.
+            <env color="Crimson"> .Map </env>
+
+            //current class during all phases, including early preprocessing
+            <crntClass color="DarkOrange"> noClass </crntClass>
+
+            // OL - location of "this" in store, or noValue in static context
+            <location color="DarkOrange"> .K </location>
+          </methodContext>
+
+          <br/>
+          //Multithreading-related cells
+
+          //Thread Id
+          <tid color="BlueViolet"> 0 </tid>
+
+          //Map[OL |-> Count] - the amount of times this thread holds the monitor objects referred bu the keys
+          <holds color="BlueViolet"> .Map </holds>
+
+          //Whether this thread was interrupted by another thread by a call to Thread.interrupt()
+          <interrupted color="BlueViolet"> false </interrupted>
+        </thread>
+      </threads>
+
+      <br/>
+      //cell type: Map[PackageId->Map[Id->ClassType]], Id = simple name, ClassType = full name
+      //Computed during ProcTypeNamesPhase. Used in all the elaboration phases.
+      <namesToClasses color="OrangeRed"> .Map </namesToClasses>
+
+      <br/>
+      <br/>
+      //Global phase Process Compilation Units
+
+      //Types imported by the current compilation unit. Created in module PROCESS-IMPORTS, part of
+      //ProcCompUnitsPhase. Used in ProcCompUnitsPhase when imports for a compilation unit are computed,
+      //and in ProcClassDecsPhase, when they are used to lookup extends/implements clauses.
+      //Type: Map[Id -> ClassType]
+      <compUnitImports color="LightCoral"> .Map </compUnitImports>
+      <br/>
+      //The local variable environment, created and used during elaboration phase.
+      //Represents a stack. Each ListItem contains a Map[Id -> Type]
+      <elabEnv color="Orange"> ListItem(mapWrap(.Map)) </elabEnv>
+
+      /*Current method/block context type - either staticCT or instanceCT
+      Used both during elaboration*/
+      <contextType color="DarkOrange"> staticCT </contextType>
+
+      //The global registry of all local classes
+      //When a local class is first encountered in the elaboration phase, a global class name is generated for it
+      //and the class is registered in this map.
+      //Type: Map[Id->ClassType] - map from simple local names to global names.
+      //Used in elaboration phase.
+      <localTypes color="Orange"> ListItem(mapWrap(.Map)) </localTypes>
+
+      //Counter used to generate unique package names for local classes. Elaboration phase only.
+      <nextLocalId color="Orange"> 1 </nextLocalId>
+
+      //A list of terms that are collected during elaboration phase by a call to appendToElabBuffer()
+      //and are restored back to <k> by a call to loadElabBuffer()
+      <elabBuffer> [.KList] </elabBuffer>
+
+      <br/>
+      <br/>
+
+
+      <classes color="Red">
+        <class multiplicity="*" color="Red">
+
+          //Class Phase Discovered
+
+          //sort ClassType. Contains the fully qualified class name.
+          <classType color="Red"> .K </classType>
+
+          //Either classMetaT or interfaceMetaT. Used in many semantics phases, including execution.
+          <classMetaType color="Maroon"> .K </classMetaType>
+
+ 	  //Class access mode - either public or package.
+          <classAccessMode color="Maroon"> .K </classAccessMode>
+
+          //The major phase of <class> lifecycle. See ClassPhase definition.
+          <classPhase color="Maroon"> .K </classPhase>
+
+          <br/>
+          //Class Phase Created
+
+          //Used by object instantiation
+          //noClass if this is a top-level class,
+          //ClassType of the enclosing class otherwise
+          <enclosingClass color="DarkGoldenrod"> noClass </enclosingClass>
+
+          <rawExtends color="DarkGoldenrod"> .K </rawExtends>
+          <rawImplements color="DarkGoldenrod"> .K </rawImplements>
+
+          //The list of class members, in their raw form.
+          <rawDeclarations color="DarkGoldenrod"> .K </rawDeclarations>
+
+          //Created in ProcCompUnitsPhase, used in ProcClassDecsPhase
+          <cuImports color="DarkGoldenrod"> .Map </cuImports> //imports of the enclosing CU, for top-level classes only.
+
+          //Either staticCT or instanceCT
+          <classContextType color="DarkGoldenrod"> .K </classContextType>
+
+
+          <br/>
+          <br/>
+          //Class phase Bases Resolved
+
+          <unprocessedBases color="Olive"> .K </unprocessedBases>
+
+          <br/>
+          <br/>
+
+          //The base class, or noClass for interfaces and Object.
+          <extends color="SpringGreen"> .K </extends>
+
+          /*Directly implemented interfaces, the resolved content of implements clause.
+            Only used during preprocessing. Mostly to compute <implTrans>, and when transitive list of
+            interfaces is not needed.*/
+          <implements color="SpringGreen"> .Set </implements>
+
+          /*Map[Id -> ClassType]. Map of classes accessible by simple name inside this class.
+            Used by type resolution in elaboration phase.*/
+          <imports color="SpringGreen"> .Map </imports>
+
+          //Transitively implemented interfaces. Used by subtyping rules.
+          <implTrans color="DeepPink"> .Set </implTrans>
+
+          /*Signatures of methods accessible to this class (both declared and inherited)
+            Map[Sig -> Class]
+            Used in elaboration of method calls.*/
+          <methods color="Blue"> .Map </methods>
+
+          <br/>
+          <br/>
+
+          /*All methods declared in this class.
+            Used in elaboration of method calls.*/
+          <methodDecs color="Blue">
+
+            <methodDec multiplicity="*" color="Blue">
+
+              //Method signature, of type Signature
+              <methodSignature color="Blue"> .K </methodSignature>
+
+	      <methodReturnType> .K </methodReturnType>
+
+              //Method params
+              <methodParams color="Blue"> .Params </methodParams>
+
+	      // first line, constructors only. Either of:
+              //   'SuperInv - superclass constructor invocation
+              //   'AltConstrInv - alternate this class constructor invocation
+              //   .K - none, if this class is Object
+              //   For methods this argument is noValue
+              //The content of this cell is moved into method body during elaboration.
+              <methodConstrFirstLine> .K </methodConstrFirstLine>
+
+              //Method body
+              <methodBody color="Blue"> .K </methodBody>
+
+              <methodAccessMode color="Blue"> .K </methodAccessMode>
+
+              //Either staticCT or instanceCT
+              <methodContextType color="Blue"> .K </methodContextType>
+
+              //Either methodMMT or constructorMMT
+              <methodMetaType> .K </methodMetaType>
+
+            </methodDec>
+          </methodDecs>
+
+          <br/>
+          <br/>
+
+          //[...,, 'LocalVarDec(_),, ...] - Instance field declarations. Used during object instantiation.
+          <instanceFields color="Indigo"> .ClassBodyDecList </instanceFields>
+	      <instanceInit color="Indigo"> .BlockStmList </instanceInit>
+
+          //[...,, 'FieldDec('Static(_),,T,,_),, ...] - Static field declarations. Used during class instantiation.
+          <staticFields color="DarkSlateGray"> .ClassBodyDecList </staticFields>
+
+          //The sequence of static initializers (that also includes field initializers)
+          //see static-init.k for more details.
+          <staticInit color="DarkSlateGray"> .BlockStmList </staticInit>
+
+          //The map of compile-time constant fields. We consider compile-time constants only final static fields
+          //initialized with a literal expression.
+          //Constant references are replaced by their values during elaboration phase.
+          //Created during process classes phase.
+          //Map[Id -> TypedVal]
+          <constantEnv color="DarkSlateGray"> .Map </constantEnv>
+
+          <br/>
+          <br/>
+          //Global phase Elaboration
+
+          //For local classes only. Map[Id -> Type] of vars accessible from the DIRECT enclosing local env.
+          //If we have more levels of Local classes nesting, more external local environments
+          //will be attached to more external classes.
+          //Used during elaboration phase only.
+          <enclosingLocalEnv color="Teal"> .Map </enclosingLocalEnv>
+
+          <br/>
+          <br/>
+          //Class Phase Execution - cells only used during execution
+
+          //Initialization status of this class. See static-init.k for more details.
+          //Only used during execution phase.
+          <staticInitStatus color="Teal"> StaticUninitialized </staticInitStatus>
+
+          /*The map of static fields declared in this class only, and NOT in superclasses or superinterfaces.
+            Map[Id -> Location] Used during static variable lookup.*/
+          <staticEnv color="DarkSlateGray"> .Map </staticEnv>
+
+        </class>
+      </classes>
+
+      <br/>
+      <br/>
+
+      //Initial cells, loaded by krun and initial configuration.
+
+      //The initial program loaded by krun. For full mode and preprocessing this is
+      //the initial java program, for execution mode it is the folded java program.
+      <program color="LightSteelBlue"> $PGM:K </program>
+
+      //Main class, passed as krun argument. We need it from the outside, just like JDK Java.
+      <mainClass color="LightSteelBlue"> $MainClass:List </mainClass>
+
+      <globalPhase color="YellowGreen"> ProcTypeNamesPhase </globalPhase>
+
+      <br/>
+      <br/>
+      //Global Phase Execution
+
+      //Execution memory. Map[Location:Int->Value:TypedVal]. Both local vars and heap vars are stored here.
+      <store color="DarkCyan"> .Map </store>
+
+      //Counter for next location to be used in the cell <store>.
+      <nextLoc color="DarkCyan"> 0 </nextLoc>
+
+      //A map from types to objectRef() terms that represent their T.class value
+      //Created an used in execution phase, by expressions of the form X.class
+      //Type: Map[Type->TypedVal]. Type may be any reference type.
+      <classLiteralsMap color="LightPink"> .Map </classLiteralsMap>
+
+      <br/>
+      <br/>
+
+      //Represents the storage of objects. Since objects have a complex inner structure,
+      //we need to hold them separately if we want to represent that structure as a cell tree.
+      <objectStore color="Cyan" map="" >
+        <object color="Cyan" multiplicity="*">
+
+          //The id of this object. Same as store location for the newly created object reference.
+          <objectId color="Cyan" key="" > .K </objectId>
+
+          //The actual object class
+          <objectType color="Cyan"> .K </objectType>
+
+          //One layer for each class in the inheritance chain of this object
+          <layer color="Cyan" multiplicity="*">
+
+            //The class corresponding to the given chain
+            <layerClass color="Cyan"> .K </layerClass>
+
+            //Map[Id |-> Loc] -> fields defined in this layer
+            <layerEnv color="Cyan"> .Map </layerEnv>
+
+            //objectRef() ::_ - a reference to the directly enclosing object, or noValue if none.
+            <layerEnclosingObject color="Cyan"> noValue:>KItem </layerEnclosingObject>
+          </layer>
+        </object>
+      </objectStore>
+
+      <arrayStore color="Cyan" map="" >
+              <array color="Cyan" multiplicity="*">
+                <arrayId color="Cyan" key="" > .K </arrayId>
+                <arrayType color="Cyan"> .K </arrayType>
+                <arraystore color="Cyan"> .Map </arraystore>
+              </array>
+      </arrayStore>
+
+      <br/>
+      <br/>
+
+      //Standard input. Each token is a ListItem.
+      <in color="LightPink" stream="stdin"> .List </in>
+
+      //Standard output. Each token is a ListItem.
+      <out color="LightPink" stream="stdout"> .List </out>
+
+      <br/>
+      <br/>
+      //Multithreading-related global cells
+
+      //Set[OL:Int] - the set of locations of used monitor objects
+      <busy color="LightGreen"> .Set </busy>
+
+      //Map[ThreadId:Int |-> OL:Int] - map from threads to objects they are waiting on
+      //waiting on those objects used by methods Object.wait(), Object.notify(), Object.notifyAll().
+      <waitingThreads color="LightGreen"> .Map </waitingThreads>
+
+      //Set[ThreadId:Int] The set of terminated threads.
+      <terminated color="LightGreen"> .Set </terminated>
+
+      <br/>
+      <br/>
+      //Cells used for debugging. Not related to the semantics.
+
+      <groupDebug color="Yellow">
+
+        <dissolveEmptyK> false </dissolveEmptyK>
+
+        //When computation finishes, dissolve all cells except <out>,
+        //in order to avoid duplicate solutions during model checking.
+        <dissolveAllExceptOut> $DissolveAllExceptOut:Bool </dissolveAllExceptOut>
+
+        <debug> .List </debug>
+
+      </groupDebug>
+    </T>
+
+endmodule
diff --git a/src/common/core-functions.k b/src/common/core-functions.k
index cfbd837c..1b26e8fe 100644
--- a/src/common/core-functions.k
+++ b/src/common/core-functions.k
@@ -258,6 +258,23 @@ rule getSimpleName(class ClassId:Id)
       rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) +Int 1
     ))
 
+/*
+Tests if a method declared in class BaseC with access mode Acc is overridden by a method
+  with the same signature declared in a subclass SubC.
+
+The method is overridden if either:
+  - Acc is protected or public
+  - Acc is package and BaseC and SubC are declared in the same package (JLS \S6.6)
+*/
+syntax KItem ::=  isOverridden (
+                ClassType,  //BaseC
+                AccessMode, //BaseAcc
+                ClassType   //SubC
+              )
+
+rule isOverridden(_, public,    _) => true
+rule isOverridden(_, protected, _) => true
+
 /*@ \subsection{Identifiers}*/
 
 // 'Id(Str:String)
diff --git a/src/common/core-sorts.k b/src/common/core-sorts.k
index c719695a..6cac931e 100644
--- a/src/common/core-sorts.k
+++ b/src/common/core-sorts.k
@@ -57,14 +57,6 @@ syntax GlobalPhase ::=
   */
   | "ElaborationPhase"
 
-  /* Folds the <class> cells into a preprocessed Java program. The last step of elaboration semantics.
-  */
-  | "FoldingPhase"
-
-  /* Unfolds each class from its preprocessed 'ClassDec or 'InterfaceDec form back into a <class> cell.
-  */
-  | "UnfoldingPhase"
-
   /* When all preprocessing / elaboration phases are finished, the actual execution begins.
   */
   | "ExecutionPhase"
diff --git a/src/common/java.k b/src/common/java.k
new file mode 100644
index 00000000..e2bee658
--- /dev/null
+++ b/src/common/java.k
@@ -0,0 +1,82 @@
+require "configuration.k"
+require "core-sorts.k"
+require "core-functions.k"
+require "core-classes.k"
+require "aux-strings.k"
+require "primitive-types.k"
+require "subtyping.k"
+require "java-syntax.k"
+
+require "../prep/core-preprocessing.k"
+require "../prep/process-type-names.k"
+require "../prep/process-comp-units.k"
+require "../prep/process-imports.k"
+require "../prep/process-class-decs.k"
+require "../prep/process-class-members.k"
+require "../prep/elaboration-categories.k"
+require "../prep/elaboration-core.k"
+require "../prep/elaboration-top-blocks.k"
+require "../prep/elaboration-statements.k"
+require "../prep/elaboration-expressions.k"
+require "../prep/elaboration-vars.k"
+require "../prep/elaboration-method-invoke.k"
+require "../prep/elaboration-new-instance.k"
+require "../prep/elaboration-arrays.k"
+require "../prep/elaboration-types.k"
+require "../prep/literals.k"
+require "../prep/process-local-classes.k"
+require "../prep/process-anonymous-classes.k"
+
+require "../exec/core-exec.k"
+require "../exec/syntax-conversions.k"
+require "../exec/to-string.k"
+require "../exec/expressions.k"
+require "../exec/expressions-classes.k"
+require "../exec/statements.k"
+require "../exec/arrays.k"
+require "../exec/static-init.k"
+require "../exec/new-instance.k"
+require "../exec/var-lookup.k"
+require "../exec/method-invoke.k"
+require "../exec/api-core.k"
+require "../exec/api-threads.k"
+
+module JAVA
+    imports CONFIGURATION
+    imports CORE-SORTS
+    imports AUX-STRINGS
+    imports PRIMITIVE-TYPES
+    imports SUBTYPING
+
+    imports JAVA-SYNTAX
+
+    imports PROCESS-TYPE-NAMES
+    imports PROCESS-COMP-UNITS
+    imports PROCESS-IMPORTS
+    imports PROCESS-CLASS-DECS
+    imports PROCESS-CLASS-MEMBERS
+    imports ELABORATION-TOP-BLOCKS
+    imports ELABORATION-STATEMENTS
+    imports ELABORATION-EXPRESSIONS
+    imports ELABORATION-VARS
+    imports ELABORATION-METHOD-INVOKE
+    imports ELABORATION-NEW-INSTANCE
+    imports ELABORATION-ARRAYS
+    imports ELABORATION-TYPES
+    imports PROCESS-LOCAL-CLASSES
+    imports PROCESS-ANONYMOUS-CLASSES
+    imports LITERALS
+
+    imports EXPRESSIONS
+    imports EXPRESSIONS-CLASSES
+    imports STATEMENTS
+    imports ARRAYS
+    imports STATIC-INIT
+    imports NEW-INSTANCE
+    imports NEW-INSTANCE-REST
+    imports VAR-LOOKUP
+    imports METHOD-INVOKE
+    imports METHOD-INVOKE-REST
+    imports API-CORE
+    imports API-THREADS
+endmodule
diff --git a/src/exec/method-invoke.k b/src/exec/method-invoke.k
index 3dad3582..b3bc4f0f 100644
--- a/src/exec/method-invoke.k
+++ b/src/exec/method-invoke.k
@@ -589,23 +589,6 @@ rule [lookupPackageMethod-new-method]:
       ...
     </class>
 
-/*
-Tests if a method declared in class BaseC with access mode Acc is overridden by a method
-  with the same signature declared in a subclass SubC.
-
-The method is overridden if either:
-  - Acc is protected or public
-  - Acc is package and BaseC and SubC are declared in the same package (JLS \S6.6)
-*/
-syntax KItem ::=  isOverridden (
-                ClassType,  //BaseC
-                AccessMode, //BaseAcc
-                ClassType   //SubC
-              )
-
-rule isOverridden(_, public,    _) => true
-rule isOverridden(_, protected, _) => true
-
 // Object class cannot match this rule since it has public access mode
 rule isOverridden(BaseC:ClassType, package, SubC:ClassType)
     => eqAux(getPackage(getTopLevel(BaseC)) , getPackage(getTopLevel(SubC)))
diff --git a/src/exec/new-instance.k b/src/exec/new-instance.k
index d891190d..09a3dca6 100644
--- a/src/exec/new-instance.k
+++ b/src/exec/new-instance.k
@@ -253,6 +253,7 @@ module NEW-INSTANCE-REST
 rule [FieldDec-instance]:
     <k> 'FieldDec(.AnnoFieldModList,, T:Type,,'VarDecList('VarDec(X:Id),, .VarDecList)) => . ...</k>
     <env> Env:Map => Env[X <- default(T) ] </env>
+    <globalPhase> ExecutionPhase </globalPhase>
 
 //@\subsection{Execution of QSuperConstrInv, AltConstrInv}
 
diff --git a/src/exec/statements.k b/src/exec/statements.k
index 8ccbc1f6..1af44af6 100644
--- a/src/exec/statements.k
+++ b/src/exec/statements.k
@@ -14,6 +14,8 @@ rule isStmt('For(_)) => true    //first argument
 
 //For now main class may only be placed in the default package.
 rule [ExecutionPhase-Start]:
+    <threads>
+    <thread>
     <k>
       //K-AST for new <MainClass>().main(new String[0]);
       . =>  getClassType(packageId(String2Id("")), String2Id(MainClassS))
@@ -24,10 +26,10 @@ rule [ExecutionPhase-Start]:
               (( new classString ([0] .DimExps)  .Dims), .Exps );
     </k>
     <env> .Map </env>
+    ...</thread>
+    </threads>
     <mainClass> ListItem(MainClassS:String) </mainClass>
-    <globalPhase> UnfoldingPhase => ExecutionPhase  </globalPhase>
-
-
+    <globalPhase> ElaborationPhase => ExecutionPhase  </globalPhase>
 
 //@ \subsection{Blocks} JLS \$14.2
 
diff --git a/src/exec/static-init.k b/src/exec/static-init.k
index e6e34a28..5c289535 100644
--- a/src/exec/static-init.k
+++ b/src/exec/static-init.k
@@ -99,5 +99,6 @@ rule [FieldDec-static]:
     <crntClass> Class:ClassType </crntClass>
     <classType> Class </classType>
     <staticEnv> Env:Map => Env[X <- default(T)] </staticEnv>
+    <globalPhase> ExecutionPhase </globalPhase>
 
 endmodule
diff --git a/src/prep/process-class-members.k b/src/prep/process-class-members.k
index 310390c5..4e421784 100644
--- a/src/prep/process-class-members.k
+++ b/src/prep/process-class-members.k
@@ -181,16 +181,6 @@ rule [isInheritable]:
     <classType> Class </classType>
     <extends> BaseClass:ClassType </extends>
 
-//A copy of isOverridden from METHOD-INVOKE
-syntax KItem ::=  isOverridden (
-                ClassType,  //BaseC
-                AccessMode, //BaseAcc
-                ClassType   //SubC
-              )
-
-rule isOverridden(_, public,    _) => true
-rule isOverridden(_, protected, _) => true
-
 // Object class cannot match this rule since it has public access mode
 rule isOverridden(BaseC:ClassType, package, SubC:ClassType)
     => eqAux(getPackage(getTopLevel(BaseC)), getPackage(getTopLevel(SubC)))
@@ -399,6 +389,7 @@ rule [FieldDec-Instance]:
     <crntClass> Class:ClassType </crntClass>
     <classType> Class </classType>
     <instanceFields> C:ClassBodyDecList => addElementToClassBodyDecListEnd(C, 'FieldDec(.AnnoFieldModList,, T,, 'VarDecList('VarDec(X:Id),, .VarDecList)) ) </instanceFields>
+    <globalPhase> ProcClassMembersPhase </globalPhase>
 when
     getContextType(Modifiers) ==K instanceCT
         [structural]
@@ -432,6 +423,7 @@ rule [FieldDec-Static]:
     <classType> Class </classType>
     <staticFields> C:ClassBodyDecList =>
     addElementToClassBodyDecListEnd(C, 'FieldDec('AnnoFieldModList('Static(.KList),, .AnnoFieldModList),, T,, 'VarDecList('VarDec(X),, .VarDecList)) ) </staticFields>
+    <globalPhase> ProcClassMembersPhase </globalPhase>
 when
     getContextType(Modifiers) ==K staticCT
         [structural]
diff --git a/src/prep/process-comp-units.k b/src/prep/process-comp-units.k
index b9dac484..464420e3 100644
--- a/src/prep/process-comp-units.k
+++ b/src/prep/process-comp-units.k
@@ -28,8 +28,8 @@ process declarations in a less-restricted order.
 
 rule [ProcCompUnitsPhase-start]:
     <k> . => Program </k>
-    (<program> Program:K </program> => .)
-     <globalPhase> ProcTypeNamesPhase => ProcCompUnitsPhase  </globalPhase>
+    <program> Program:K => . </program>
+    <globalPhase> ProcTypeNamesPhase => ProcCompUnitsPhase </globalPhase>
 
 //ImpDecs will be processed in the module PROCESS-IMPORTS
 rule [CompilationUnit]:
diff --git a/src/prep/process-type-names.k b/src/prep/process-type-names.k
index 8375bfea..30dd7ee5 100644
--- a/src/prep/process-type-names.k
+++ b/src/prep/process-type-names.k
@@ -15,6 +15,13 @@ The initial configuration contains the initial program in cells <k> and <program
 /*@ \subsection{Compilation units}*/
 
 // 'CompilationUnit('Some('PackageDec(_,, Pack:PackageId)),, _)
+rule [start]:
+        <threads>
+          . => <thread> <k> Program </k> ...</thread>
+        </threads>
+        <program> Program:K </program>
+    <globalPhase> ProcTypeNamesPhase </globalPhase>
+
 rule [CompilationUnit-DefaultPackage-Desugar]:
     'CompilationUnit(
       ( 'None(_) => 'Some('PackageDec(.AnnoList,, 'PackageName( .IdList ))) ),,
diff --git a/tools/kjrun.sh b/tools/kjrun.sh
index 6828649a..85c8592a 100755
--- a/tools/kjrun.sh
+++ b/tools/kjrun.sh
@@ -50,9 +50,6 @@ function setSearchPattern() {
   fi
 }
 
-#If true then we have to run preprocessing semantics first
-PREP_FIRST=true
-
 TIME=true
 
 # OS-dependent choice of timeout
@@ -63,11 +60,7 @@ fi
 TIMEOUT=$((120 * $TIMEOUT_FACTOR))
 SEARCH_TIMEOUT_FACTOR=2
 
-MODE=run-exec
-PREP_OUTPUT=kast
-OUTPUT=pretty
-PREP_INPUT=java
-INPUT=kast
+INPUT=java
 
 # Pattern example: "<T> <out> OUT:List </out> _</T>"
 PATTERN=""
@@ -83,15 +76,7 @@ CLEAN=false
 #If true then we display the built command in kjrun and aux-kjrun
 VERBOSE=false
 
-#If true then don't show any messages besides the actual output
-SILENT=false
-
 CMD_SUFFIX=""
-COUNT_CMD_SUFFIX="| grep \"Solution\" | wc -l"
-PREP_AST_CMD_SUFFIX="| sed 's/\s*\([[:graph:]].*[[:graph:]]\)\s*/\1/g'"
-PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | tr -d '\n'"
-PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | sed -r 's/.*<program>//g' | sed -r 's/<\/program>.*//g'"
-PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | sed 's/KListWrap/ListWrap/g'"
 
 while [[ ${1:0:1} == - ]]; do
   PARAM=`echo $1 | awk -F= '{print $1}'`
@@ -104,31 +89,7 @@ while [[ ${1:0:1} == - ]]; do
       usage
       exit
       ;;
-    "--prep-ast")
-      PREP_FIRST=false
-      MODE=run-prep-ast
-      CMD_SUFFIX=${PREP_AST_CMD_SUFFIX}
-      OUTPUT=kast
-      INPUT=java
-      TIME=false
-      TIMEOUT=0
-
-      ;;
-    "--prep-pretty")
-      PREP_FIRST=false
-      MODE=run-prep-config
-      INPUT=java
-      ;;
-    "--prep-raw")
-      PREP_FIRST=false
-      MODE=run-prep-config
-      OUTPUT=kast
-      INPUT=java
-      ;;
-    "--exec-pretty")
-      PREP_FIRST=false
-      MODE=run-exec
-      ;;
+ 
     "--split") #everything default
       ;;
     "--split-cached")
@@ -136,26 +97,12 @@ while [[ ${1:0:1} == - ]]; do
       TIMEOUT=0
       PREP_INPUT=kast-cache
       OUTPUT=none
-      SILENT=true
       ;;
     "--split-none")
       PREP_INPUT=kast-cache
       OUTPUT=none
       ;;
-    "--search")
-      TIMEOUT=$(($TIMEOUT * $SEARCH_TIMEOUT_FACTOR))
-      MODE=search
-      setSearchPattern
-      ;;
-    "--search-cached")
-      TIME=false
-      TIMEOUT=0
-      PREP_INPUT=kast-cache
-      MODE=search
-      CMD_SUFFIX=${COUNT_CMD_SUFFIX}
-      SILENT=true
-      setSearchPattern
-      ;;
+
     "--debug")
       TIME=false
       TIMEOUT=0
@@ -172,7 +119,6 @@ while [[ ${1:0:1} == - ]]; do
       PREP_INPUT=kast-cache
       MODE=symbolic
       CMD_SUFFIX=${COUNT_CMD_SUFFIX}
-      SILENT=true
       setSearchPattern
       ;;
 
@@ -212,48 +158,39 @@ if [[ ${JAVA_FILE} == "" ]]; then
 fi
 
 BASE_JAVA_FILE=`basename ${JAVA_FILE}`  #simple file/dir name
-PKAST_FILE=`echo "$BASE_JAVA_FILE" | sed 's#/*$##'` # remove trailing slashes, important if JAVA_FILE is dir
-PKAST_FILE=${PKAST_FILE}.pkast
+MAIN_CLASS=`echo "$BASE_JAVA_FILE" | cut -d'.' -f1` #simple file minus extension
+TOOLS_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+WORK_DIR="$(pwd)"
 
+SEMANTICS_DIR=$(cross-path-native.sh ${TOOLS_DIR}/../src/common)
 
-#Actual execution
-if [[ ${SILENT} == false ]]; then
-  echo "preprocess:"
+# OS-dependent selection of krun.
+if !(( $TIME == false )); then
+ KRUN_CMD="time"
 fi
 
-if [[ ${PREP_FIRST} == true ]]; then
-  if [ ! -e ${PKAST_FILE} ]; then
-    CMD="aux-kjrun.sh --time=${TIME} --timeout=${TIMEOUT} --mode=run-prep-ast --output=${PREP_OUTPUT} \
-      --cmd-suffix=\"${PREP_AST_CMD_SUFFIX}\" \
-      --input=${PREP_INPUT} --verbose=${VERBOSE} ${JAVA_FILE} > ${PKAST_FILE}"
-    if [[ ${VERBOSE} == true ]]; then
-      echo "PREP cmd:"
-      echo ${CMD}
-      echo
-    fi
-    eval ${CMD}
-  fi
-else
-  PKAST_FILE=${JAVA_FILE}
-fi
+KRUN_CMD="$KRUN_CMD timeout $TIMEOUT"
 
-if [[ ${SILENT} == false ]]; then
-  echo
-  echo "execute:"
-  echo
-fi
+KRUN_CMD="$KRUN_CMD $(cross-k.sh krun)"
+
+KRUN_CMD="$KRUN_CMD --directory \"$SEMANTICS_DIR\""
 
-CMD="aux-kjrun.sh --time=${TIME} --timeout=${TIMEOUT} --mode=${MODE} --output=${OUTPUT} --input=${INPUT} \
-  --pattern=\"${PATTERN}\" --ltlmc=\"${LTLMC}\" --config=\"${CONFIG}\" \
-  --verbose=${VERBOSE} --cmd-suffix=\"${CMD_SUFFIX}\" ${PKAST_FILE}"
-if [[ ${VERBOSE} == true ]]; then
-  echo "EXEC cmd:"
-  echo ${CMD}
-  echo
+if (( $OUTPUT == "none" )); then
+KRUN_CMD="$KRUN_CMD --output none"	
 fi
 
+KRUN_CMD="$KRUN_CMD --symbolic-execution -w none"
+
+KRUN_CMD="$KRUN_CMD --parser \"$(cross-sh.sh kj-parse-aggreg.sh)\""
+
+KRUN_CMD="$KRUN_CMD -cMainClass=\"ListItem(\\\"$MAIN_CLASS\\\")\""
+
+KRUN_CMD="$KRUN_CMD -cDissolveAllExceptOut=\"true\""
+
+KRUN_CMD="$KRUN_CMD $JAVA_FILE"
+
 # Actual command evaluation
-eval ${CMD}
+eval ${KRUN_CMD}
 
 if [[ ${CLEAN} == true ]]; then
   rm -rf *.kast