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

Cardinality of Int #130

Closed pkriens closed 3 years ago

pkriens commented 3 years ago

While playing with the Evaluator I noticed that #Int = 0. This seems to also have some effect on the model since:

 run { # Int > 0 }

Does not provide an instance

aleksandarmilicevic commented 3 years ago

That's because #Int is always 0! (mind blowing)

In Alloy, instead of specifying individual int atoms, only a bitwidth is specified. When the specified bitwidth is b, the Int set becomes . The cardinality of that set is .

  1. With the "Prevent Overflows" option turned off (i.e., using the wraparound semantics)
    • #Int is 2^b, which is exactly 0 when integers wrap around, thus #Int > 0 is unsatisfiable
  2. With the "Prevent Overflows" option turned on
    • #Int is 2^b, which clearly overflows, and so #Int > 0 is unsatisfiable
    • if you already have an instance and then in the evaluator evaluate #Int, the evaluator will print out 0 and say that overflow happened.
pkriens commented 3 years ago

stupid of me ...