nicolasdilley / Gomela

Tool developped for "Bounded verification of message passing concurrency in Go programs."
39 stars 7 forks source link

Fix missing fors and restructured cross-model properties #24

Open VladSaioc opened 1 year ago

VladSaioc commented 1 year ago

A key problem was that model cloning sometimes led to lost properties. To avoid this, a model structure also carries a pointer to a structure remembering global values (e.g. contains mutex/wg/channel), which is then propagated to any models cloned from the current one.