[Bug] Instance Translator cannot properly set exact scope for top-level signatures more than one
ferhaterata opened this issue · 1 comments
ferhaterata commented
sig Requirement {
requires: set Requirement,
refines: set Requirement,
contains: set Requirement,
partiallyRefines: set Requirement,
conflicts: set Requirement,
equals: set Requirement
}
sig Implementation {
satisfy: set Requirement,
refines: set Implementation,
}
The scope fragment of generated Alloy code for above top-level signatures using Reason@relation and ConsistencyChecking functions is in the following:
...
pred show{}
run show for
exactly 14 Requirement
Instead, that should be as in the following:
...
pred show{}
run show for
exactly 14 Requirement, 0 Implementation
ferhaterata commented
There is no bug. False Alarm because of the user changed the specification without uploading the specification.