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

IllegalArgumentException in forthcoming CLI #226

Closed grayswandyr closed 4 months ago

grayswandyr commented 6 months ago

@pkriens in commit 654e00b, when running command exec (without further argument) on the following model, an exception is raised:

enum State { Idle, Wait, Crit }

sig Process {
        var state: one State,
}

var one sig token in Process {}

pred ask[p: Process] {
        p.state = Idle
        state' = state ++ p->Wait
        token' = token
}

fact transitions {
        always some p: Process | ask[p] 
}

check { 
        all p: Process | always (p.state = Wait implies eventually p.state = Crit) }

solving command Check check$1
   207 vars. 20 primary vars. 342 clauses.
   434 vars. 34 primary vars. 780 clauses.
   629 vars. 48 primary vars. 1153 clauses.
   825 vars. 62 primary vars. 1540 clauses.
   1060 vars. 76 primary vars. 2004 clauses.
   1243 vars. 90 primary vars. 2383 clauses.
   1430 vars. 104 primary vars. 2773 clauses.
   1616 vars. 118 primary vars. 3168 clauses.
   2011 vars. 132 primary vars. 4102 clauses.
   2250 vars. 146 primary vars. 4661 clauses.
   UNSAT!
[main] ERROR alloy - excuting sub command CLI:exec error java.lang.IllegalArgumentException: y 1 is too high, max 1
java.lang.IllegalArgumentException: y 1 is too high, max 1
    at org.alloytools.util.table.Canvas.bounds(Canvas.java:261)
    at org.alloytools.util.table.Canvas.get(Canvas.java:249)
    at org.alloytools.util.table.Canvas.merge(Canvas.java:226)
    at org.alloytools.util.table.Canvas.line(Canvas.java:207)
    at org.alloytools.util.table.Canvas.line(Canvas.java:175)
    at org.alloytools.util.table.Canvas.box(Canvas.java:164)
    at org.alloytools.util.table.Table.render(Table.java:93)
    at org.alloytools.util.table.Table.render(Table.java:87)
    at org.alloytools.util.table.Table.render(Table.java:109)
    at org.alloytools.util.table.Table.toString(Table.java:168)
    at org.alloytools.util.table.Table.toString(Table.java:82)
    at aQute.lib.io.IO.store(IO.java:1062)
    at aQute.lib.io.IO.store(IO.java:1054)
    at aQute.lib.io.IO.store(IO.java:1044)
    at org.alloytools.alloy.cli.CLI.generate(CLI.java:265)
    at org.alloytools.alloy.cli.CLI._exec(CLI.java:180)
    at aQute.lib.getopt.CommandLine.execute(CommandLine.java:158)
    at org.alloytools.alloy.core.infra.AlloyDispatcher.__alloy(AlloyDispatcher.java:132)
    at aQute.lib.getopt.CommandLine.execute(CommandLine.java:158)
    at org.alloytools.alloy.core.infra.AlloyDispatcher.main(AlloyDispatcher.java:94)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.base/java.lang.reflect.Method.invoke(Method.java:566)
    at org.alloytools.alloy.core.infra.Alloy.main(Alloy.java:73)
Error
  0. [Canvas.bounds] executing CLI:exec
pkriens commented 4 months ago

There was no check that the solution was satisfiable so I tried to show a non-sat, and there was an assumption in the toString that there was a sat.