How to create a new instance of a variable signature

I want to create a new instance of a variable signature. For example, I want to spawn a subprocess as in the following model:

var sig Process {
	var subprocess : lone Process
}

pred spawnSubprocessInstance(p:Process) {
	// Try to spawn a new subprocess x of p, i.e., set p.subprocess = x.
	Process' = p + {x:Process { p.subprocess' = x}}
}

pred init [] {
	some p:Process { p.subprocess = none }
	#Process = 1
}

pred trans [] {
	(some p:Process  | spawnSubprocessInstance[p])
	or
	doNothing
}

pred doNothing [] {
	Process' = Process
}

pred System {
	init and always trans
}

run System

However, the method I am currently using does not seem to work. So, my question is, how can I create an instance of a variable signature and add a relation to an old instance? In usual programming, I would call a constructor to create a new object. I can force creation by #Process’ = 2, but then I cannot add a relation.

Thanks in advance. It feels like I am missing something obvious or have misunderstood something.

Hi tim,

I usually do it as follows:

pred spawnSubprocessInstance(p:Process) {
	// Try to spawn a new subprocess x of p, i.e., set p.subprocess = x.
	some x : Process'-Process {
		Process' = Process + x
		subprocess' = subprocess + p->x
	}
}

The set Process'-Process contains the new processes and by quantifying over this set your force x to be a new process. The constraint Process' = Process + x forces this set to contain a single new process. The constraint subprocess' = subprocess + p->x adds a new tuple to the subprocess relation. An alternative formulation could be:

pred spawnSubprocessInstance(p:Process) {
	// Try to spawn a new subprocess x of p, i.e., set p.subprocess = x.
	one (Process' - Process) // there is a single new process
	let x = Process'-Process { // let x be that new process
		subprocess' = subprocess + p->x
	}
}

Btw, in your doNothing predicate you should also force subprocess to not change, by adding subprocess' = subprocess.

Best,
Alcino

1 Like

Thanks, Alcino! This is exactly what I was looking for :slight_smile: