Eddie
Results
1
comments of
Eddie
The issue in general-model was, we only allow clients writes to its own region. The write() macro should be fix with this: ```tla (* Regular write at write region *)...