tmp

Makefile

@@ -56,17 +56,17 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
 
-# TODO: Add $(EXECUTION_INPUT_DIR)/$(shell echo "%" | sed 's/\.[^.]*$$//').rs
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
 # as a dependency
 $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP)
 	mkdir -p $(EXECUTION_OUTPUT_DIR)
 	krun \
-		$(EXECUTION_INPUT_DIR)/$(shell echo "%" | sed 's/\.[^.]*$$//').rs \
+		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
 		--definition $(RUST_EXECUTION_KOMPILED) \
 		--output kore \
 		--output-file $@.tmp \
 		-cTEST="$(shell cat $<)" \
-		-pTEST=./run-test.sh
+		-pTEST=$(CURDIR)/run-test.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
 

rust-semantics/targets/execution/configuration.md

@@ -2,13 +2,13 @@
 
 module RUST-RUNNING-CONFIGURATION
     imports private RUST-PREPROCESSING-SYNTAX
-    imports private RUST-EXECUTION-TEST-EXECUTION-SYNTAX
+    imports private RUST-EXECUTION-TEST-PARSING-SYNTAX
     imports RUST-CONFIGURATION
     imports RUST-EXECUTION-TEST-CONFIGURATION
 
     configuration
         <rust-mx>
-            <k> crateParser($PGM:Crate) ~> runTest($TEST:ExecutionTest) </k>
+            <k> crateParser($PGM:Crate) ~> $TEST:ExecutionTest </k>
             <rust/>
             <rust-test/>
         </rust-mx>

rust-semantics/test/execution.md

@@ -9,19 +9,16 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "call" TypePath "." Identifier
 endmodule
 
-module RUST-EXECUTION-TEST-EXECUTION-SYNTAX
-    imports RUST-EXECUTION-TEST-PARSING-SYNTAX
-
-    syntax Executor ::= runTest(ExecutionTest)
-endmodule
-
 module RUST-EXECUTION-TEST
     imports LIST
-    imports RUST-EXECUTION-TEST-EXECUTION-SYNTAX
+    imports RUST-EXECUTION-TEST-PARSING-SYNTAX
     imports RUST-HELPERS
     imports RUST-REPRESENTATION
     imports RUST-RUNNING-CONFIGURATION
 
+    rule E:ExecutionItem ; Es:ExecutionTest => E ~> Es
+    rule .ExecutionTest => .K
+
     rule
         <k> new P:TypePath => .K ... </k>
         <test-stack> .List => ListItem(NVI) ... </test-stack>