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

cnf export does not handle mutuable signatures and fields #183

Open goens opened 2 years ago

goens commented 2 years ago

I was exporting some models that were taking a long time to solve to CNF to check with an external solver. I was surprised when, for models I knew instances existed, the solver returned that they were unsatisfiable.

I then noticed that the exported CNF instances are identical independent of the number of steps I give them.

A simple example to reproduce:

sig B {}
sig A{ var b : set B }

fact init { no b }
pred step { some bval : B | bval not in A.b and A.b' = A.b + bval }
pred end { A.b = B}
fact stepsuntilend { step until end and eventually end }

run {} for exactly 3 A,  exactly 2 B, 3 steps
run {} for exactly 3 A,  exactly 2 B, 1 steps

The first one will find an instance just fine, while the second one won't (as 1 step is not enough). However, exporting to CNF will produce the same SAT instance (corresponding to one step, I presume).

goens commented 2 years ago

By the way, this issue does not show up when exporting to Kodkod.

grayswandyr commented 2 years ago

Pinging @nmacedo