Minigrid2PRISM
Installation
Download the current version of Minigrid2PRISM from github:
git clone https://github.com/PrangerStefan/Minigrid2PRISM
The binary is built using CMake:
cd Minigrid2PRISM
mkdir build
cd build
cmake ..
make
Usage
Minigrid2PRISM translates a textual representation of a MinigridSafe environment into the PRISM modelling language. You can find a complete manual of the language on the PRISM website.
The HelloLavaGap environment below is a simple example, used to showcase the translation into the PRISM modelling language.
The environment is a 4x4 grid world, with lava pools and a goal.
We model the agent in its environment by the means of modules
.
A symbolic model of this environment needs to describe the agents position in the grid, as well as its viewing direction.
We use three variables to do so:
module Agent
colAgent : [1..4];
rowAgent : [1..4];
viewAgent : [0..3];
The agents movement can now be modelled by so-called commands. A command describes an action that the agent can potentially execute. For example, if the agent is looking to the north, which is internally encoded by a value of 3 of the viewAgent variable, it has not yet entered a lava or goal state, and it is not blocked by a wall, it may move to the north:
[Agent_move_North] viewAgent=3 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
Using Minigrid2PRISM, we can automatically create a complete model of the environment, by calling:
./Minigrid2PRISM -i grid.txt -o HelloLavaGap.prism
Note, that when using tempestpy, the model generation is fully automated by the ShieldHandler.
The complete model for the HelloLavaGap environment can be concisely represented as such:
mdp
formula AgentCannotMoveEastWall = (colAgent=4&rowAgent=1) | (colAgent=4&rowAgent=2) | (colAgent=4&rowAgent=3) | (colAgent=4&rowAgent=4);
formula AgentCannotMoveNorthWall = (colAgent=3&rowAgent=1) | (colAgent=4&rowAgent=1) | (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1);
formula AgentCannotMoveSouthWall = (colAgent=1&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=4&rowAgent=4) | (colAgent=2&rowAgent=4);
formula AgentCannotMoveWestWall = (colAgent=1&rowAgent=2) | (colAgent=1&rowAgent=3) | (colAgent=1&rowAgent=4) | (colAgent=1&rowAgent=1);
formula AgentIsOnSlippery = false;
formula AgentIsOnLava = (colAgent=2&rowAgent=1) | (colAgent=2&rowAgent=3) | (colAgent=2&rowAgent=4);
formula AgentIsOnGoal = (colAgent=4&rowAgent=4);
init
true
endinit
module Agent
colAgent : [1..4];
rowAgent : [1..4];
viewAgent : [0..3];
[Agent_turn_right] !AgentIsOnLava &true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
[Agent_turn_left] !AgentIsOnLava &viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
[Agent_turn_left] !AgentIsOnLava &viewAgent=0 -> 1.000000: (viewAgent'=3);
[Agent_move_North] viewAgent=3 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
[Agent_move_East] viewAgent=0 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveEastWall -> 1.000000: (colAgent'=colAgent+1);
[Agent_move_South] viewAgent=1 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1);
[Agent_move_West] viewAgent=2 & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1);
endmodule