X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=code%2FSokobanObjectwise.icl;h=15fb732e63b2f230d023c634a381dacff171a7c3;hb=a7a9fa5ded371c89459ba6872290774488ec7c3d;hp=9dc09a1105dca15d0715ba7afe3ca8702b233a6c;hpb=7cfce42112573a44475b35240aad128e77f64917;p=mc1516pa.git diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl index 9dc09a1..15fb732 100644 --- a/code/SokobanObjectwise.icl +++ b/code/SokobanObjectwise.icl @@ -24,25 +24,45 @@ 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", + encodeObVar "agent" maxX maxY, + join "\n" [encodeObVar ("b" <+ i) maxX maxY\\i<-boxnums], "\tmovement: {left, up, right, down, finished};", - "\tagent: " <+ encodeAgent annot, - encodeBoxes boxes, - - "DEFINE", - "\tdx := case", + "--Handy variable for deltas", + deltaDefine, + "--Initial values", + "INIT", + encodeObInit "agent" agent <+ " &", + join " &\n" [encodeObInit ("b" <+ i) p\\p<-boxes & i<-[0..]], + "--Agent not on the box", + "INVAR " <+ encodeAgentNotOnBox boxnums <+ ";", + "--Allowed box positions on the field", + join "\n" ["INVAR "<+encodeObPosition ("b"<+b) legalPos<+";"\\b<-boxnums], + "--Box not on box", + encodeBoxOnBoxes (indexList boxes), + "--Allowed agent positions", + "INVAR " <+ encodeObPosition "agent" legalPos, + "--Goal state", + "INVAR " <+ encodeGoalState boxnums targetPos <+ ";", + "", + encodeObMovement "agent", + 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 + +deltaDefine :: String +deltaDefine = join "\n" [ + "DEFINE dx := case", "\t\tmovement = left : -1;", "\t\tmovement = right: +1;", "\t\tTRUE: 0;", @@ -51,24 +71,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 +87,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 +97,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 +108,52 @@ 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] + +encodeObMovement :: String -> String +encodeObMovement s = "TRANS next(" <+ s <+ "x) = " <+ s <+ "x + dx;\n" <+ + "TRANS next(" <+ s <+ "y) = " <+ s <+ "y + dy;" + +encodeObPosition :: String [(Int, Int)] -> String +encodeObPosition b p = join " |\n\t" [forThisX b x p\\x<-removeDup $ map fst p] + where + forThisX :: String Int [(Int, Int)] -> String + forThisX s cx p = "(" <+ s <+ "x=" <+ cx <+ " & (" <+ + join " | " [s <+ "y=" <+ y \\(x, y)<-p | x == cx] <+ "))" -encodeObjectPositions :: [(Int, Int)] -> String -encodeObjectPositions p = join " | " ["x="<+x<+" & "<+"y="<+y\\(x, y)<-p] +encodeObInit :: String (Int, Int) -> String +encodeObInit s (x, y) = "\t" <+ s <+ "x=" <+ x <+ " & " <+ s <+ "y=" <+ y -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 +encodeObVar :: String Int Int -> String +encodeObVar s mx my = "\t" <+ s <+ "x: 0.." <+ mx <+ ";\n" <+ + "\t" <+ s <+ "y: 0.." <+ my <+ ";\n" -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;"