From: Mart Lubbers Date: Mon, 14 Mar 2016 20:40:39 +0000 (+0100) Subject: added model X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ac86d6c040926676fa06911b0e49888021620652;p=mc1516pa.git added model --- diff --git a/Models/489-coord.smv b/models/489-coord.smv similarity index 100% rename from Models/489-coord.smv rename to models/489-coord.smv diff --git a/models/489-object.smv b/models/489-object.smv new file mode 100644 index 0000000..2acc7fc --- /dev/null +++ b/models/489-object.smv @@ -0,0 +1,104 @@ +MODULE ob(ix, iy) +VAR + x: 0..7; + y: 0..7; +INIT x=ix & y=iy +INVAR (x=0 & (y=0 | y=5 | y=6 | y=7)) | + (x=1 & (y=0 | y=2 | y=3 | y=7)) | + (x=3 & (y=1 | y=2 | y=3 | y=5)) | + (x=4 & (y=1 | y=2 | y=3 | y=4 | y=5 | y=6)) | + (x=5 & (y=1 | y=2 | y=4 | y=5 | y=6)) | + (x=2 & (y=2 | y=3 | y=4 | y=5 | y=7)) | + (x=6 & (y=2 | y=3 | y=4)) + +MODULE main +VAR + agent: ob(4, 3); + b0: ob(2, 2); + b1: ob(3, 2); + b2: ob(3, 5); + b3: ob(4, 5); + movement: {left, up, right, down, finished}; +--Handy variable for deltas +DEFINE dx := case + movement = left : -1; + movement = right: +1; + TRUE: 0; + esac; + dy := case + movement = up : -1; + movement = down: +1; + TRUE: 0; + esac; +--Agent not on the box +INVAR !(b0.x = agent.x & b0.y = agent.y) & + !(b1.x = agent.x & b1.y = agent.y) & + !(b2.x = agent.x & b2.y = agent.y) & + !(b3.x = agent.x & b3.y = agent.y); +--Box not on box +INVAR !(b0.x=b1.x &b0.y=b1.y) & !(b0.x=b2.x &b0.y=b2.y) & !(b0.x=b3.x &b0.y=b3.y) & + !(b1.x=b2.x &b1.y=b2.y) & !(b1.x=b3.x &b1.y=b3.y) & + !(b2.x=b3.x &b2.y=b3.y) & + TRUE; +--Goal state +INVAR ((b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) | + (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) | + (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) | + (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) | + (b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) | + (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) | + (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) | + (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) | + (b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) | + (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) | + (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) | + (b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) | + (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) | + (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) | + (b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) | + (b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) | + (b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) | + (b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) | + (b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) | + (b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) | + (b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5) | + (b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) | + (b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) | + (b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5))<->movement=finished; +--Agent movement +TRANS next(agent.x) = agent.x + dx & next(agent.y) = agent.y + dy; +--Box movement +TRANS next(b0.x) = case + next(agent.x) = b0.x & next(agent.y) = b0.y: b0.x + dx; + TRUE: b0.x; + esac; +TRANS next(b0.y) = case + next(agent.x) = b0.x & next(agent.y) = b0.y: b0.y + dy; + TRUE: b0.y; + esac; +TRANS next(b1.x) = case + next(agent.x) = b1.x & next(agent.y) = b1.y: b1.x + dx; + TRUE: b1.x; + esac; +TRANS next(b1.y) = case + next(agent.x) = b1.x & next(agent.y) = b1.y: b1.y + dy; + TRUE: b1.y; + esac; +TRANS next(b2.x) = case + next(agent.x) = b2.x & next(agent.y) = b2.y: b2.x + dx; + TRUE: b2.x; + esac; +TRANS next(b2.y) = case + next(agent.x) = b2.x & next(agent.y) = b2.y: b2.y + dy; + TRUE: b2.y; + esac; +TRANS next(b3.x) = case + next(agent.x) = b3.x & next(agent.y) = b3.y: b3.x + dx; + TRUE: b3.x; + esac; +TRANS next(b3.y) = case + next(agent.x) = b3.x & next(agent.y) = b3.y: b3.y + dy; + TRUE: b3.y; + esac; +CTLSPEC ! EF (movement = finished); +