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 123 forks source link

Implement an improved translation to SMV directly in Pardinus #197

Open grayswandyr opened 1 year ago

grayswandyr commented 1 year ago

Currently, the translation to SMV backends is performed by an OCaml program. Furthermore, this program doesn't handle models featuring integers.

This issue is here to track a re-implementation in Pardinus/Java, also handling ints. Technically it's a Pardinus issue but we also need to keep track of it for the Alloy Analyzer.

grayswandyr commented 1 year ago

Reminder:

sig S{ var r : S}

check {
always (#S = 4)
} for 3 Int, exactly 4 S

yields no counterexample because the (current_ translation of # into count does not take the bound on Int into account.

grayswandyr commented 1 year ago

Recall Skolemizing too: this won't compile with Electrod

sig S { var r : set S}
run { some s : set S | some s } for 3 Int

fails. Electrod:

electrod (C) 2016-2020 ONERA 1.0.0-1-geb0b02e
[E002] 00000.elo:23.13-23.20: syntax error this##S
       (some s: set this##S { 
Aborting (1.973ms).