From c2f18e81f24962057945dc3fbf48d00a0f03537c Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sat, 12 Mar 2016 12:22:30 +0100 Subject: [PATCH] works, tested with 2000 and 642 --- code/SokobanObjectwise.icl | 149 ++++++++++++++++++++++--------------- 1 file changed, 88 insertions(+), 61 deletions(-) diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl index 9dc09a1..7297c32 100644 --- a/code/SokobanObjectwise.icl +++ b/code/SokobanObjectwise.icl @@ -24,25 +24,13 @@ Start w encode :: SokobanPuzzle -> String encode p = join "\n" [ - "MODULE ob(ix, iy, movement)", - "VAR", - "\tx: 0 .. " <+ maxX <+ ";", - "\ty: 0 .. " <+ maxX <+ ";", - - "INVAR " <+ encodeObjectPositions legalPos <+ ";", - - "ASSIGN", - "\tinit(x):=ix;", - "\tinit(y):=iy;\n", - "MODULE main", "VAR", + encodeAgentVars maxX maxY, + encodeBoxVars (indexList boxes) maxX maxY, "\tmovement: {left, up, right, down, finished};", - "\tagent: " <+ encodeAgent annot, - encodeBoxes boxes, - - "DEFINE", - "\tdx := case", + "", + "DEFINE dx := case", "\t\tmovement = left : -1;", "\t\tmovement = right: +1;", "\t\tTRUE: 0;", @@ -52,20 +40,30 @@ encode p = join "\n" [ "\t\tmovement = down: +1;", "\t\tTRUE: 0;", "\tesac;", - - "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ - ") <-> movement = finished;", + "", + "INIT", + encodeAgentInit agent <+ " &", + encodeBoxInit boxes <+ ";", + "--Agent not on the box", "INVAR " <+ encodeAgentNotOnBox (indexList boxes) <+ ";", - "INVAR " <+ encodeBoxesNotOnBox (indexList boxes), - "TRANS next(agent.x) = agent.x + dx;", - "TRANS next(agent.y) = agent.y + dy;", - encodeBlockMovement (indexList boxes), - "CTLSPEC ! EF (movement = finished)", - "CTLSPEC EF (b0.x=3)" - ] + "--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 @@ -84,6 +82,9 @@ getTargets p = [(x, y)\\(x, y, t)<-p | getMetrics :: AnnotatedSokoban -> (Int, Int) getMetrics p = (maximum (map fst3 p),maximum (map snd3 p)) +getAgents :: AnnotatedSokoban -> [(Int, Int)] +getAgents p = [(x, y)\\(x, y, Agent)<-p] ++ [(x, y)\\(x, y, TargetAgent)<-p] + getBoxes :: AnnotatedSokoban -> [(Int, Int)] getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p] @@ -91,7 +92,8 @@ getBoxes p = [(x, y)\\(x, y, Box)<-p] ++ [(x, y)\\(x, y, TargetBox)<-p] (<+) a b = toString a +++ toString b encodeGoalState :: [Int] [(Int, Int)] -> String -encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets +encodeGoalState boxes targets = "(" <+ + join " |\n\t" (map encodeOneGoal boxtargets) <+ ")<->movement=finished" where boxtargets = map (zip2 targets) (permutations boxes) @@ -101,44 +103,69 @@ encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets encodeOneGoal` :: [((Int, Int), Int)] -> [String] encodeOneGoal` [] = [] encodeOneGoal` [((x, y), b):xs] = [ - "b" <+ b <+ ".x = " <+ x <+ " & " <+ - "b" <+ b <+ ".y = " <+ y:encodeOneGoal` xs] - - -encodeBlockMovement :: [Int] -> String -encodeBlockMovement bs = join "\n" $ map ebm bs + "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 - ebm :: Int -> String - ebm i = - "TRANS next(b" <+ i <+ ".x) = case\n" <+ - "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+ - "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+ - "\t\tTRUE: b" <+ i <+ ".x + dx;\n" <+ - "\tesac;\n" <+ - "TRANS next(b" <+ i <+ ".y) = case\n" <+ - "\t\tnext(agent.x) != b" <+ i <+ ".x | " <+ - "next(agent.y) != b" <+ i <+ ".y: b" <+ i <+ ".x;\n" <+ - "\t\tTRUE: b" <+ i <+ ".y + dy;\n" <+ - "\tesac;" - -//TODO -encodeBoxesNotOnBox :: [Int] -> String -encodeBoxesNotOnBox _ = "TRUE;" + 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 != agent.x & b" <+ i <+ ".y != agent.y)"\\i<-bs] + "!(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;" -encodeObjectPositions :: [(Int, Int)] -> String -encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p] +encodeBoxInit :: [(Int,Int)] -> String +encodeBoxInit bs = join " &\n" [ + "\tb" <+ i <+ "x=" <+ x <+ " & " <+ + "b" <+ i <+ "y=" <+ y + \\(x, y)<-bs & i<-[0..]] -encodeAgent :: AnnotatedSokoban -> String -encodeAgent [x:xs] = case x of - (x, y, Agent) = "ob(" <+ x <+ "," <+ y <+ ", movement);" - (x, y, TargetAgent) = "ob(" <+ x <+ "," <+ y <+ ", movement);" - _ = encodeAgent xs +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] -encodeBoxes :: [(Int, Int)] -> String -encodeBoxes p = join "\n" - ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);" - \\(bx, by)<-p & i<-[0..]] +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;" -- 2.20.1