Bulk static data

Questions
1

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.

2

In Alloy, the main ways to fix (partially or totally) a problem are either to use one sigs or to rely on existential quantification (typically a some disj room1, room2, link1, ... | link1.src_room = room1 and ...).

An issue is that we can’t fix the value or fields this way (only as formulas) but you could do this in Kodkod (the solver underlying Alloy, available as a standalone JAR at Emina Torlak’s web page).

Related to this topic, notice that Alloy 6 features a Decompose strategy option (due to @nmacedo and @alcino) that, if set to parallel may leverage your CPU cores to perform solving on exact instances (“configurations”) of your problem (thus solving some constraints at construction time). YMMV, but this is sometimes useful if your problem is not completely fixed, in particular when expecting the analysis to be SAT (to yield an instance or counterexample).