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

JSON output not including instances #253

Closed awwaiid closed 5 months ago

awwaiid commented 5 months ago

The -t json option is a great idea! However, it doesn't appear to be outputting instances. I've done this testing off of #249, which appears to be the most functional current branch.

Here is a console session:

awwaiid@vorm:~/projects/recurse/org.alloytools.alloy$ cat simple.als                                                                                                         [nmacedo/master]
sig Thing {} run { one Thing }
awwaiid@vorm:~/projects/recurse/org.alloytools.alloy$ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar exec simple.als                               [nmacedo/master]
solving command Run run$1
[main] INFO kodkod.engine.config.Reporter - detecting symmetries ...
[main] INFO kodkod.engine.config.Reporter - detected 17 equivalence classes of atoms ...
[main] INFO kodkod.engine.config.Reporter - optimizing bounds and formula (breaking predicate symmetries, inlining, skolemizing) ...
[main] INFO kodkod.engine.config.Reporter - translating to boolean ...
[main] INFO kodkod.engine.config.Reporter - generating lex-leader symmetry breaking predicate ...
[main] INFO kodkod.engine.config.Reporter - translating to cnf ...
   14 vars. 3 primary vars. 15 clauses.
   SAT!
repeat -2
answers 1
[main] INFO kodkod.engine.config.Reporter - solving p cnf 14 16
---
Command                                 Run run$1
Duration (ms)                           73
Sequence                                0
┌────┬─────┬─────────────────────┐
│loop│state│instance             │
├────┼─────┼──────────┬──────────┤
│true│0    │sig       │fields    │
│    │     ├──────────┼──────────┤
│    │     │this/Thing│this/Thing│
│    │     │          ├──────────┤
│    │     │          │Thing²    │
└────┴─────┴──────────┴──────────┘

awwaiid@vorm:~/projects/recurse/org.alloytools.alloy$ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar exec -t json simple.als                       [nmacedo/master]
solving command Run run$1
[main] INFO kodkod.engine.config.Reporter - detecting symmetries ...
[main] INFO kodkod.engine.config.Reporter - detected 17 equivalence classes of atoms ...
[main] INFO kodkod.engine.config.Reporter - optimizing bounds and formula (breaking predicate symmetries, inlining, skolemizing) ...
[main] INFO kodkod.engine.config.Reporter - translating to boolean ...
[main] INFO kodkod.engine.config.Reporter - generating lex-leader symmetry breaking predicate ...
[main] INFO kodkod.engine.config.Reporter - translating to cnf ...
   14 vars. 3 primary vars. 15 clauses.
   SAT!
repeat -2
answers 1
[main] INFO kodkod.engine.config.Reporter - solving p cnf 14 16
[
  {
    "bitwidth":4,
    "command":"Run run$1",
    "incremental":true,
    "instances":[
      {
        "skolems":{

        },
        "state":0,
        "values":{
          "Int":{

          },
          "String":{

          },
          "none":{

          },
          "seq/Int":{

          },
          "this/Thing":{

          },
          "univ":{

          }
        }
      }
    ],
    "localtime":"2024-04-10T14:17:06.301324348",
    "loopstate":-1,
    "module":{
      "name":"unknown",
      "opens":[
        {
          "module":{
            "name":"util/integer",
            "opens":[

            ],
            "path":"integer"
          },
          "parameters":[

          ]
        }
      ],
      "path":""
    },
    "overflow":false,
    "root":null,
    "satisfiable":true,
    "sigs":{
      "univ":{
        "builtin":true,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"univ",
        "type":"{univ}"
      },
      "Int":{
        "builtin":true,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"Int",
        "type":"{Int}"
      },
      "seq/Int":{
        "builtin":true,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"seq/Int",
        "type":"{seq/Int}"
      },
      "String":{
        "builtin":true,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"String",
        "type":"{String}"
      },
      "none":{
        "builtin":true,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"none",
        "type":"{none}"
      },
      "this/Thing":{
        "builtin":false,
        "cardinality":"set",
        "fields":{

        },
        "isEnum":false,
        "meta":false,
        "name":"this/Thing",
        "type":"{this/Thing}"
      }
    },
    "skolemDepth":0,
    "solver":"sat4j",
    "unrolls":-1,
    "utctime":1712773026296
  }
]%            

You can see that even though there is an instance in the regular text/table output, the json output doesn't have anything. This appears true for any model I've tried.

awwaiid commented 5 months ago

Ah -- I think the issue is around instances which have no fields. Here is a model that has a field:

sig Thing {
    id: Int
}
run example { some Thing }

With that, here is a fragment of the json output:

{
  "bitwidth":4,
  "command":"Run example",
  "incremental":true,
  "instances":[
    {
      "skolems":{

      },
      "state":0,
      "values":{
        "Int":{

        },
        "String":{

        },
        "none":{

        },
        "seq/Int":{

        },
        "this/Thing":{
          "id":{
            "arity":2,
            "data":[
              [
                "Thing$0",
                "6"
              ],
              [
                "Thing$0",
                "6"
              ]
            ]
          }
        },
...

So you can see that once it has some fields it does fill in some nested values.

The relevant text output here is:

this/Thing={Thing$0, Thing$1}
this/Thing<:id={Thing$0->6, Thing$1->5}

And the text output for the original model which has no fields:

this/Thing={Thing$0, Thing$1}

I'm wondering what this JSON should look like to be nice and clean. Let's say you have ThingNoField and ThingWithField. Maybe

{
  "instances": [
    {
      "skolems": {},
      "state": 0,
      "values": {
        "this/ThingNoField": [
          {
            "label": "ThingNoField$0",
            "fields": {}
          },
          {
            "label": "ThingNoField$1",
            "fields": {}
          }
        ],
        "this/ThingWithField": [
          {
            "label": "ThingWithField$0",
            "fields": {
              "id": "6"
            }
          },
          {
            "label": "ThingWithField$1",
            "fields": {
              "id": "7"
            }
          }
        ]
      }
    }
  ]
}

Though I suspect I am missing something in the correct way to serialize instances, this feels like the way I think of an instance of having some label and some fields and those fields have values.

pkriens commented 5 months ago

Fixed