I’m looking for idioms or best practices for building Alloy models that depend on a large pile of static data (i.e. constrained to be constant across all instances).
Currently, I’m specifying the static part of my model by generating a large .als file with a bunch of "one sig … extends … {} { … } " declarations that instantiate and configure a bunch of objects. I’m happy with the resulting semantics, but I think I could get better (problem construction time) performance. This setup works, but it does so by building a giant SAT problem with a huge number of variables/constraints that enforce the one configuration I want. I’d rather somehow specify my static data in a way that allows simplifications at problem construction time rather than waiting until solving time.
To make this question concrete, I’ll briefly describe a concrete scenario I’m working with. I’m trying to model the ways of interacting in a videogame world where the player can move between rooms, hopping from one abstract waypoint/node to another based on how they use items in their inventory.
The interesting part of the world design is expressed with a bunch of statement like this: “You can move from [Room1,Node2] to [Room3,Node4] using [Way5 or Way6 or Way7], where Way5 requires [Item9 and Item10], etc.” I’m trying to ask questions like “can the player get softlocked / enter a room from which they can never leave?” The presence of a softlock depends on the entire world design in non-obvious ways. I know that softlocks can exist generally, but I want to find them (or verify their absence) in specific full-scale world designs.
Here’s the formulation for the static/unchanging part of my model (numbers are taken from the real-world application):
abstract sig Item {}
abstract sig Way { requires: set Item }
abstract sig Room {}
abstract sig Node {}
abstract sig Door extends Node {}
abstract sig Drop extends Node { item: Item }
abstract sig Link { src_room, dst_room: Room, src_node, dst_node: Node, ways: set Way }
run {} for
exactly 30 Door,
exactly 36 Drop,
exactly 255 Room,
exactly 33 Item,
exactly 254 Way,
exactly 1538 Link
Running unconstrained (exactly as above), this model takes about 1 minute to build. When I extend it with a bunch of “one sig” declarations that force a configuration of every object, it then takes 12 minutes to build the constraint problem (after which the solving time less than one second). Surely there should be a way of writing down my static data such that providing more information reduces problem construction time.
I’d love it if there were a quick hack like “use macros” or “use multirelations”, but general advice on making data-dependent models would also help.