Skip to content

Changing how the independent function is translated #13

@nicolasdilley

Description

@nicolasdilley

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) {
...
}`

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions