How to create a new instance of a variable signature

Questions
1

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.

2

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

4 Likes
3

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

4

Pardon my reviving the topic, but does the spawn need framing condition too? I am thinking along the line of

pred spawnSubprocessInstance(p:Process) {
	some x : Process' - Process {
		Process' = Process + x
		subprocess' = subprocess + p->x
	}
    // Frame: Keep all other subprocess relations unchanged
    all x : Process' & Process {
        x.subprocess' = x.subprocess
    }
}

Oh nevermind, subprocess' = subprocess + p->x already constrains subprocess' properly.

What I am thinking about is a somewhat OOP mimic way of writing which necessitates it:

pred spawnSubprocessInstance(p:Process) {
    // Effect: New Process
    some x : Process' - Process {
        Process' = Process + x
        p.subprocess' = x
    }
    // Frame: Keep all other subprocess relations unchanged
    all x : Process' & Process {
        x.subprocess' = x.subprocess
    }
}

I think I will give up the mimic, the extra framing needed is too much with more “properties”.

5

It’s what we use to call a relational update. It’s nice as the frame condition is already present in it, which is both shorter and less error-prone.

1 Like