search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
694 stars 122 forks source link

A run command with growing scopes should stop once an instance is found #231

Open SteveZhangBit opened 5 months ago

SteveZhangBit commented 5 months ago

Here is a minimal test scenario:

sig A {}

run {} for 3..5 A

My question is what is the expected semantic for a scoped command? I expect that the model gradually increases the bound for A to find a solution. This is useful when I don't know the possible minimum bound for a signature.

So I expect that when 3 atoms of A would be satisfiable, the solver returns a solution. However, the actual behavior is it searches for 3, 4, and 5 As.

This is the line of code that I think causes this "issue": https://github.com/AlloyTools/org.alloytools.alloy/blame/654e00b0338985c85457b246d154a9457c4a3299/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java#L509

nmacedo commented 3 months ago

This feature was never officially documented (as far as I know), so I'm not sure what was the initial intention. But I agree that a run command with growing scopes should stop once an instance is found. That's actually what happens in check commands with growing scopes, it stops at the first counter-example found.

grayswandyr commented 2 months ago

Renamed the issue. Setting it as a possible enhancement.