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
695 stars 124 forks source link

run foo for n does not set bitwidth #138

Closed edmcman closed 1 year ago

edmcman commented 3 years ago

I was very confused by the fact that this model did not find any instances:

sig Dummy {}

pred example { #Dummy = 8 }
run example for 10 //but 5 int

The problem is that run example for N does not increase the bitwidth, so N > 7 is useless without increasing the bitwidth. Perhaps a warning should be issued, or the bitwidth should automatically be increased?

grayswandyr commented 1 year ago

IMO, we should issue a warning for every command featuring integers that does not set the bitwidth explictly.

grayswandyr commented 1 year ago

Tracked in #30 .