X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanObjectwise.icl;h=656fad8312292a46978193aad47dc031f358488b;hb=3350e67ad7c96bf9b821c0d691a58eb141a13e17;hp=9dc09a1105dca15d0715ba7afe3ca8702b233a6c;hpb=4211e0aeed639a9eb14488d456cd95bdffc16118;p=mc1516pa.git diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl index 9dc09a1..656fad8 100644 --- a/code/SokobanObjectwise.icl +++ b/code/SokobanObjectwise.icl @@ -24,25 +24,48 @@ Start w encode :: SokobanPuzzle -> String encode p = join "\n" [ - "MODULE ob(ix, iy, movement)", + "MODULE ob(ix, iy)", "VAR", - "\tx: 0 .. " <+ maxX <+ ";", - "\ty: 0 .. " <+ maxX <+ ";", - - "INVAR " <+ encodeObjectPositions legalPos <+ ";", - - "ASSIGN", - "\tinit(x):=ix;", - "\tinit(y):=iy;\n", - + "\tx: 0.." <+ maxX <+ ";", + "\ty: 0.." <+ maxY <+ ";", + "INIT x=ix & y=iy", + "INVAR " <+ encodeObPosition legalPos, + "", "MODULE main", "VAR", + "\tagent: " <+ declareObject agent, + join "\n" ["\tb" <+ i <+ ": " <+ declareObject b\\i<-boxnums & b<-boxes], "\tmovement: {left, up, right, down, finished};", - "\tagent: " <+ encodeAgent annot, - encodeBoxes boxes, - - "DEFINE", - "\tdx := case", + "--Handy variable for deltas", + deltaDefine, + "--Agent not on the box", + "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";", + "--Box not on box", + "INVAR " <+ encodeBoxOnBoxes boxnums <+ ";", + "--Goal state", + "INVAR " <+ encodeGoalState boxnums targetPos <+ ";", + "--Agent movement", + encodeObMovement "agent", + "--Box movement", + encodeBoxMovement boxnums, + "CTLSPEC ! EF (movement = finished);", + + ""] + where + targetPos = getTargets annot + boxes = getBoxes annot + boxnums = indexList boxes + agent = hd $ getAgents annot + legalPos = legalPositions annot + annot = annotate p + (maxX, maxY) = getMetrics annot + +declareObject :: (Int, Int) -> String +declareObject (x, y) = "ob(" <+ x <+ ", " <+ y <+ ");" + +deltaDefine :: String +deltaDefine = join "\n" [ + "DEFINE dx := case", "\t\tmovement = left : -1;", "\t\tmovement = right: +1;", "\t\tTRUE: 0;", @@ -51,24 +74,7 @@ encode p = join "\n" [ "\t\tmovement = up : -1;", "\t\tmovement = down: +1;", "\t\tTRUE: 0;", - "\tesac;", - - "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ - ") <-> movement = finished;", - "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)" - ] - where - targetPos = getTargets annot - boxes = getBoxes annot - legalPos = legalPositions annot - annot = annotate p - (maxX, maxY) = getMetrics annot + "\tesac;"] //THIS IS NAIVE AND SHOULD BE IMPROVED legalPositions :: AnnotatedSokoban -> [(Int, Int)] @@ -84,6 +90,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 +100,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) @@ -103,42 +113,43 @@ encodeGoalState boxes targets = join " |\n\t" $ map encodeOneGoal boxtargets 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 +encodeBoxOnBoxes :: [Int] -> String +encodeBoxOnBoxes [] = "" +encodeBoxOnBoxes [b] = "TRUE" +encodeBoxOnBoxes [b:bs] = encodeBoxOnBox b bs <+ " &\n\t" <+ + 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 = agent.x & b" <+ i <+ ".y = agent.y)"\\i<-bs] -encodeObjectPositions :: [(Int, Int)] -> String -encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p] +encodeObMovement :: String -> String +encodeObMovement s = "TRANS next(" <+ s <+ ".x) = " <+ s <+ ".x + dx & " <+ + "next(" <+ s <+ ".y) = " <+ s <+ ".y + dy;" -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 +encodeObPosition :: [(Int, Int)] -> String +encodeObPosition p = join " |\n\t" [forThisX x p\\x<-removeDup $ map fst p] + where + forThisX :: Int [(Int, Int)] -> String + forThisX cx p = "(x=" <+ cx <+ " & (" <+ + join " | " ["y=" <+ y \\(x, y)<-p | x == cx] <+ "))" -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(agent.x) = b" <+ i <+ ".x & " <+ + "next(agent.y) = 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(agent.x) = b" <+ i <+ ".x & " <+ + "next(agent.y) = b" <+ i <+ ".y: b" <+ i <+ ".y + dy;\n" <+ + "\t\tTRUE: b" <+ i <+ ".y;\n" <+ + "\tesac;"