instead of modelling the body of the independent function in the init,
the init proctype could be used to initialise the communication parameters of the function and spawn an instance of a proctype which models the body of the independent function.
for _, machine := range machines {
numConcurrentActions++ /<\label{line:dep-inc}>/
go machineCommand(actionName, machine, errorChan) /<\label{line:dep-go}>/
}
for i := 0; i < numConcurrentActions; i++ { /<\label{line:dep-for}>/
err := <-errorChan /<\label{line:dep-rcv}>/
if err != nil {
errs = append(errs, err)
}
}
instead of modelling the body of the independent function in the init, the init proctype could be used to initialise the communication parameters of the function and spawn an instance of a proctype which models the body of the independent function.
IE. if modelling function
` func runActionForeachMachine(actionName string, machines []host.Host) []error { var ( numConcurrentActions = 0 /<\label{line:dep-var}>/ errorChan = make(chan error) /<\label{line:dep-chan}>*/ errs = []error{} )
for _, machine := range machines { numConcurrentActions++ /<\label{line:dep-inc}>/ go machineCommand(actionName, machine, errorChan) /<\label{line:dep-go}>/ }
for i := 0; i < numConcurrentActions; i++ { /<\label{line:dep-for}>/ err := <-errorChan /<\label{line:dep-rcv}>/ if err != nil { errs = append(errs, err) } }
close(errorChan)
return errs }
func machineCommand(actionName string, host *host.Host, errorChan chan<- error) { ... } `
could be modelled as
`
define machines_4 ??
define numConcurrentActions_6 ??
init { runActionForeachMachines(machines_4,numConcurrentActions_6) }
proctype runActionForEachMachines(int machines, int numConcurrentActions) { ... }`