From: Mart Lubbers Date: Fri, 11 Mar 2016 10:12:01 +0000 (+0100) Subject: almost finished code, strange error X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f299e4212080c6cff79893ba99cebe7ab18a500e;p=mc1516pa.git almost finished code, strange error --- diff --git a/code/.gitignore b/code/.gitignore index dacd0be..6c83100 100644 --- a/code/.gitignore +++ b/code/.gitignore @@ -1,3 +1,4 @@ Clean System Files a.out SokobanObjectwise +*.prj diff --git a/code/SokobanObjectwise.icl b/code/SokobanObjectwise.icl index 558cc4f..d51ee55 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,117 @@ 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 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", + "\tmovement: {left, up, right, down, finished};", + "\tagent: " <+ encodeAgent annot, + encodeBoxes boxes, + + "DEFINE", + "\tdx := 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;", + + "INVAR (" <+ encodeGoalState (indexList boxes) targetPos <+ + ") <-> movement = finished;", + "INVAR " <+ encodeAgentNotOnBox (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 -:: 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] ++ - - where - getBox` _ [] = [] - getBox` x [b:bs] = let r = getBox` (x+1) bs in case b of - Box = [x:r] - TargetBox = [x:r] - _ = r +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 + 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] + + +encodeBlockMovement :: [Int] -> String +encodeBlockMovement 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;\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;" + +encodeAgentNotOnBox :: [Int] -> String +encodeAgentNotOnBox bs = join " &\n\t" [ + "(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] + +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 + +encodeBoxes :: [(Int, Int)] -> String +encodeBoxes p = join "\n" + ["\tb" <+ i <+ ": ob(" <+ bx <+ ", " <+ by <+ ", movement);" + \\(bx, by)<-p & i<-[0..]]