Repair/RepairCompiler/MCC/specs/freeciv/test.model

   1 [], true => map in MAP;
   2 [forall m in MAP], true => m.tiles in GRID;
   3 [forall t in GRID, for x=0 to map.xsize-1, for y=0 to map.ysize-1], true => t.grid[x+(y*map.xsize)] in TILE;
   4 [forall t in TILE], true => <t,t.terrain> in TERRAIN;
   5 [forall t in TILE], !(t.city = NULL) => <t,t.city> in CITYMAP;
   6 [forall t in TILE], !(t.city = NULL) => t.city in CITY;