X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanObjectwise.icl;h=7297c3206c8488fb3a5f428f6c33e4a0ab42536f;hb=c2f18e81f24962057945dc3fbf48d00a0f03537c;hp=558cc4f2c83430b78602fb9239f5969ed109038a;hpb=fd2b1775e5bd5172560e2cb3e2d0878d46a50b60;p=mc1516pa.git

diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl
index 558cc4f..7297c32 100644
--- a/code/SokobanObjectwise.icl
+++ b/code/SokobanObjectwise.icl
@@ -6,8 +6,15 @@ import StdTuple
 import StdFunc
 import StdOrdList
 import StdList
+
+from Data.Func import $
+from Data.List import intercalate, maximum, permutations
+from Text import class Text(concat,join), instance Text String
+
 import Sokoban
 
+:: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
+
 Start :: *World -> *World
 Start w
 # (io, w) = stdio w
@@ -16,36 +23,149 @@ Start w
 = snd (fclose io w)
 
 encode :: SokobanPuzzle -> String
-encode p = foldr ((+++) o (+++) "\n") "" ([
-	"MODULE", 
-	"main",
-	"VAR":encodeBoxes p maxX maxY])
+encode p = join "\n" [
+	"MODULE main",
+	"VAR",
+	encodeAgentVars maxX maxY,
+	encodeBoxVars (indexList boxes) maxX maxY,
+	"\tmovement: {left, up, right, down, finished};",
+	"",
+	"DEFINE dx := case",
+	"\t\tmovement = left : -1;",
+	"\t\tmovement = right: +1;",
+	"\t\tTRUE:              0;",
+	"\tesac;",
+	"\tdy := case",
+	"\t\tmovement = up  : -1;",
+	"\t\tmovement = down: +1;",
+	"\t\tTRUE:             0;",
+	"\tesac;",
+	"",
+	"INIT",
+	encodeAgentInit agent <+ " &",
+	encodeBoxInit boxes <+ ";",
+	"--Agent not on the box",
+	"INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";",
+	"--Allowed box positions on the field",
+	encodeBoxPositions (indexList boxes) legalPos,
+	"--Box not on box",
+	encodeBoxOnBoxes (indexList boxes),
+	"--Allowed agent positions",
+	"INVAR " <+ encodeAgentPositions legalPos,
+	"--Goal state",
+	"INVAR " <+ encodeGoalState (indexList boxes) targetPos <+ ";",
+	"",
+	encodeAgentMovement,
+	encodeBoxMovement (indexList boxes),
+	"CTLSPEC ! EF (movement = finished);",
+
+	""]
 	where
+		targetPos = getTargets annot
+		boxes = getBoxes annot
+		agent = hd $ getAgents annot
+		legalPos = legalPositions annot
 		annot = annotate p
 		(maxX, maxY) = getMetrics annot
 
-:: AnnotatedSokoban :== [(Int, Int, SokobanTile)]
+//THIS IS NAIVE AND SHOULD BE IMPROVED
+legalPositions :: AnnotatedSokoban -> [(Int, Int)]
+legalPositions p = [(x, y)\\(x, y, t)<-p | case t of Wall=False; _=True]
 
 annotate :: SokobanPuzzle -> AnnotatedSokoban
 annotate (Sokoban p) = flatten [[(x, y, t)\\t<-r & x<-[0..]]\\r<-p & y<-[0..]]
 
+getTargets :: AnnotatedSokoban -> [(Int, Int)]
+getTargets p = [(x, y)\\(x, y, t)<-p | 
+	case t of Target=True;TargetBox=True;TargetAgent=True;_=False] 
+
 getMetrics :: AnnotatedSokoban -> (Int, Int)
-getMetrics p = (maxList (map fst3 p),maxList (map snd3 p))
+getMetrics p = (maximum (map fst3 p),maximum (map snd3 p))
 
-getBoxes :: AnnotatedSokoban -> [(Int, Int)]
-getBoxes p = [t\\t=:(_, _, Box)<-p] ++ 
+getAgents :: AnnotatedSokoban -> [(Int, Int)]
+getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p]
 
-	where
-		getBox` _ [] = []
-		getBox` x [b:bs] = let r = getBox` (x+1) bs in case b of
-				Box = [x:r]
-				TargetBox = [x:r]
-				_ = r
+getBoxes :: AnnotatedSokoban -> [(Int, Int)]
+getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p]
 
 (<+) infixr 5 :: a b -> String | toString a & toString b
 (<+) a b = toString a +++ toString b
 
-encodeBoxes :: SokobanPuzzle Int Int -> [String]
-encodeBoxes p mx my = [
-	"\tbox" <+ i <+ "x: " <+ "0 .. " <+ mx <+ ";\n\tbox" <+
-	i <+ "y: " <+ "0 .. " <+ my <+ ";"\\(bx, by)<-getBoxes p & i<-[0..]]
+encodeGoalState :: [Int] [(Int, Int)] -> String
+encodeGoalState boxes targets = "(" <+
+	join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished"
+	where
+		boxtargets = map (zip2 targets) (permutations boxes)
+		
+		encodeOneGoal :: [((Int, Int), Int)] -> String
+		encodeOneGoal p = "(" <+ join " & " (encodeOneGoal` p) <+ ")"
+
+		encodeOneGoal` :: [((Int, Int), Int)] -> [String]
+		encodeOneGoal` [] = []
+		encodeOneGoal` [((x, y), b):xs] = [
+			"b" <+ b <+ "x = " <+ x <+ " & " <+
+			"b" <+ b <+ "y = " <+ y:encodeOneGoal` xs]
+
+encodeBoxOnBoxes :: [Int] -> String
+encodeBoxOnBoxes [] = ""
+encodeBoxOnBoxes [b] = ""
+encodeBoxOnBoxes [b:bs] = "INVAR " <+ encodeBoxOnBox b bs <+ ";\n" <+
+	encodeBoxOnBoxes bs
+	where
+		encodeBoxOnBox :: Int [Int] -> String
+		encodeBoxOnBox x bs = join " & " ["!(b" <+ x <+ "x=b" <+ b <+ "x &" <+ 
+			"b" <+ x <+ "y=b" <+ b <+ "y)"\\b<-bs]
+
+encodeAgentNotOnBox :: [Int] -> String
+encodeAgentNotOnBox bs = join " &\n\t" [
+	"!(b" <+ i <+ "x = agentx & b" <+ i <+ "y = agenty)"\\i<-bs]
+
+encodeObPosition :: String [(Int, Int)] -> String
+encodeObPosition b p = join " | " [
+	"(" <+ b <+ "x=" <+ x <+ " & " <+
+	b <+ "y=" <+ y <+ ")"\\ (x, y)<-p]
+
+encodeAgentInit :: (Int, Int) -> String
+encodeAgentInit (x, y) = "\tagentx=" <+ x <+ " & " <+ "agenty=" <+ y
+
+encodeAgentVars :: Int Int -> String
+encodeAgentVars mx my = 
+	"\tagentx: 0.." <+ mx <+ ";\n\tagenty: 0.." <+ my <+ ";\n"
+
+encodeAgentPositions :: [(Int, Int)] -> String
+encodeAgentPositions p = encodeObPosition "agent" p
+
+encodeAgentMovement :: String
+encodeAgentMovement = "TRANS next(agentx) = agentx + dx;\n" <+
+	"TRANS next(agenty) = agenty + dy;"
+
+encodeBoxInit :: [(Int,Int)] -> String
+encodeBoxInit bs = join " &\n" [
+	"\tb" <+ i <+ "x=" <+ x <+ " & " <+
+	"b" <+ i <+ "y=" <+ y
+	\\(x, y)<-bs & i<-[0..]]
+
+encodeBoxVars :: [Int] Int Int -> String
+encodeBoxVars p mx my = join "\n" 
+	["\tb" <+ i <+ "x: 0.." <+ mx <+ ";\n" <+
+	"\tb" <+ i <+ "y: 0.." <+ my <+ ";" \\ i<-p]
+	
+encodeBoxPositions :: [Int] [(Int, Int)] -> String
+encodeBoxPositions bs ps = join "\n" [
+	"INVAR " <+ encodeObPosition ("b" <+ b) ps <+ ";"\\b<-bs]
+
+encodeBoxMovement :: [Int] -> String
+encodeBoxMovement bs = join "\n" $ map ebm bs
+	where
+		ebm :: Int -> String
+		ebm i =
+			"TRANS next(b" <+ i <+ "x) = case\n" <+
+			"\t\tnext(agentx) = b" <+ i <+ "x & " <+
+			"next(agenty) = b" <+ i <+ "y: b" <+ i <+ "x + dx;\n" <+
+			"\t\tTRUE: b" <+ i <+ "x;\n" <+
+			"\tesac;\n" <+
+			"TRANS next(b" <+ i <+ "y) = case\n" <+
+			"\t\tnext(agentx) = b" <+ i <+ "x & " <+
+			"next(agenty) = b" <+ i <+ "y: b" <+ i <+ "y + dy;\n" <+
+			"\t\tTRUE: b" <+ i <+ "y;\n" <+
+			"\tesac;"