ModelWriter/WP3

[Bug] Instance Translator cannot properly set exact scope for top-level signatures more than one

ferhaterata opened this issue · 1 comments

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

There is no bug. False Alarm because of the user changed the specification without uploading the specification.