Alloy model of space trading simulation game

interstellar.als

-- This a mostly-faithful translation of interstellar.lp from https://gist.github.com/rndmcnlly/cc801233012df3cb0883
-- Integer-indexed orbitals were dropped in favor of systems just having a set of planets because the order isn't interesting.

-- This first block of definitions defines the static configuration of the story world.

sig Commodity {}
private enum Equipment { Jumpdrive }
private enum Location { Orbit, Surface }
fun shuttleDestination: Location -> one Location { Orbit -> Surface + Surface -> Orbit }

sig Planet {
	produces: Location -> Commodity,
	consumes: Location -> Commodity,
	transduces: Location -> Commodity -> Commodity,
	sells: Equipment -> Int
} {
	#produces <= 2
	#consumes <= 2
	#transduces <= 1
	#sells <= 1
}

sig System {
	jumpgates: set System - this,
	planets: disj set Planet,
}

-- This block sets up how actions can be taken over time to change the state stored in a Step.

enum Action { EnterOrbit, LeaveOrbit, Shuttle, Jump, Gather, Trade, Tranduce, Buy }

let unchanged[r] { r' = r }

one sig Step {
	var location: lone Location,
	var planet: lone Planet,
	var system: one System,
	var inventory:  set Commodity + Equipment,
	var wealth: one Int,

	var action: Action,
	var object: lone System + Planet + Commodity + Equipment
}{
	always {
		action = EnterOrbit => {
			-- enter orbit of a specific planet in this system after being adrift in system
			no location
			no planet
			object in system.planets

			location' = Orbit
			planet' = object
			unchanged[system]
			unchanged[inventory]
			unchanged[wealth]
		}
		action = LeaveOrbit => {
			-- leave current planet, resulting in being adrift in the system
			location = Orbit
			some planet

			no location'
			no planet'
			unchanged[system]
			unchanged[inventory]
			unchanged[wealth]
		}
		action = Shuttle => {
			-- toggle beween orbit and surface of current planet
			no object

			location' = shuttleDestination[location]
			unchanged[planet]
			unchanged[system]
			unchanged[inventory]
			unchanged[wealth]
		}
		action = Jump => {
			-- jump to another system, adrift before and after
			some object :> System
			Jumpdrive in inventory
			no location
			no planet
			object in system.jumpgates
			

			unchanged[location]
			unchanged[planet]
			system' = object
			unchanged[inventory]
			unchanged[wealth]
		}
		action = Gather => {
			-- gain a produced item you don't already have
			some object :> Commodity
			object in planet.produces[location]
			object not in inventory

			unchanged[location]
			unchanged[planet]
			unchanged[system]
			inventory' = inventory + object
			unchanged[wealth]
		}
		action = Trade => {
			-- provide a consumed object you have, growing wealth
			some object :> Commodity
			object in planet.consumes[location]
			object in inventory

			unchanged[location]
			unchanged[planet]
			unchanged[system]
			inventory' = inventory - object
			wealth' = smaller[4,plus[wealth,1]]
		}
		action = Tranduce => {
			-- convert a one tranduced item into another
			some object :> Commodity
			some object.(planet.transduces[location])
			object in inventory

			unchanged[location]
			unchanged[planet]
			unchanged[system]
			inventory' = inventory + planet.transduces[location][object] - object
			unchanged[wealth]
		}
		action = Buy => {
			-- gain sold equipment, but don't lose wealth
			some object :> Equipment
			some planet.sells[object]
			wealth >= planet.sells[object]
			
			unchanged[location]
			unchanged[planet]
			unchanged[system]
			inventory' = inventory + object
		}
	}
}

-- This block forces a specific static configuration of the world and finds a story/plan where a special item is finally collected.

pred story {
	some disj EtaRavioli, Sol, Corea: System |
	some disj Earth, Mars, Belt, Jupiter, MeatballOne, Cloud, Ring: Planet |
	some disj Trinkets, Water, Hydrogen, Rocks, Rustbuckets, Urnoxen, UrnoxHides: Commodity {

		jumpgates =
			Sol -> EtaRavioli +
			EtaRavioli -> Sol  +
			Sol -> Corea
		
		planets =
			Sol -> (Earth + Mars + Belt + Jupiter) +
			EtaRavioli -> (MeatballOne + Cloud) +
			Corea -> Ring
	
		produces =
			Earth -> Surface -> Trinkets +
			Earth -> Surface -> Water +
			Jupiter -> Orbit -> Hydrogen +
			Belt -> Orbit -> Rocks +
			Mars -> Orbit -> Rustbuckets +
			MeatballOne -> Surface ->  Urnoxen
	
		transduces =
			MeatballOne -> Surface -> Urnoxen -> UrnoxHides
	
		consumes =
			Ring -> Surface -> UrnoxHides +
			Earth -> Surface -> Rustbuckets +
			Belt -> Orbit -> Hydrogen +
			Jupiter -> Orbit -> Rocks

		sells = Belt -> Jumpdrive -> 4
		
		Step.location = Surface
		Step.planet = Earth	
		Step.system = Sol
		no Step.inventory
		Step.wealth = 1

		eventually {
			UrnoxHides in Step.inventory
		}
	}
	
}

run {story} 
	for exactly 3 System
	, exactly 7 Planet
	, exactly 7 Commodity
	, 25 steps