From 42226c6b60be11b2d59dd37eb94d728ebd6bc023 Mon Sep 17 00:00:00 2001
From: Virgil Serbanuta <Virgil Serbanuta>
Date: Fri, 23 Aug 2024 00:22:33 +0300
Subject: [PATCH] tmp

---
 Makefile                                          |  6 +++---
 rust-semantics/targets/execution/configuration.md |  4 ++--
 rust-semantics/test/execution.md                  | 11 ++++-------
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/Makefile b/Makefile
index f171b41..8b5664e 100644
--- a/Makefile
+++ b/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 $@
 
diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md
index e3ab03d..2ad60e6 100644
--- a/rust-semantics/targets/execution/configuration.md
+++ b/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>
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index 0292677..8aa1dc7 100644
--- a/rust-semantics/test/execution.md
+++ b/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>