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.
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.