Beginner stuck on traces

1

I am totally new to this side of the programming world but very interested. I am trying to get my hands dirty so to speak by modeling system that associates papers by the search strategy used to originally retrieve the papers.
Toy-ness aside, I am having trouble generating instances based on an empty initial state. Below is the code that I have so far. Running with no system predicate, alloy is able to generate seemingly arbitrary instances however. Could someone help me diagnose the problem with the model I have written?
Thanks in advance!

sig SearchStrategy {
	strat: Strat,
	version: Int,
	var papers: some Paper
}
sig Strat {}
sig Paper {
	pmid: PID,
	var searchStrats: some SearchStrategy,
	var field: set Field,
}
sig PID {}
abstract sig Field {}

sig Author extends Field {
	name: String 
}

pred add_paper[p: Paper] {
	-- preconditions	
	not (p in SearchStrategy.papers)

	-- postconditions
	Paper' = Paper + p
	SearchStrategy.papers' = SearchStrategy.papers + p	
}

pred init {
	no Paper
	no SearchStrategy
}
// Transitions
pred trans {
	(some p: Paper | add_paper[p]) 
}

// Denotes all possible executions of the system from an initial condition state
pred System {
	init 
	always trans
}

run { System } for 5
2

There are various issues and there are probably several ways to solve them :

  • Paper and SearchStrategy are static (immutable) but you seem to expect Paper can change through add_paper.
  • Also you’re saying in init that Paper is empty but also, in trans, that in every state there is some paper p such that…, but if Paper is empty, this won’t do it.
  • Also, taking a p in Paper to add it to Paper is certainly not what you mean.
  • Not a source of inconsistency, but SearchStrategy.papers' = SearchStrategy.papers + p seems problematic too. Notice that it doesn’t say that search strategies are left as is except that you add p for some search strategy. For instance, in the first state, you could have papers = { ss1->q } and in the next state: papers = { ss1->p, ss2->q } (mind the ss2).