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.
When you specify the integer bitwidth in alloy, it always gives you signed integers, ie writing run {} for 3 Int will give you {-4, ... 3}. Many models only need the positive integers, so we'd get more state space coverage by allowing unsigned integers.
Example spec:
sig Resource {
cost: Int
}
run {sum[univ.cost] <= 5} for 3 Int
This will give a lot of specs where Resources have negative costs, and there's no way for a Resource to cost 4.
When you specify the integer bitwidth in alloy, it always gives you signed integers, ie writing
run {} for 3 Int
will give you{-4, ... 3}
. Many models only need the positive integers, so we'd get more state space coverage by allowing unsigned integers.Example spec:
This will give a lot of specs where Resources have negative costs, and there's no way for a Resource to cost 4.