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
696 stars 124 forks source link

Alloy Analyzer crash #134

Closed vazirim closed 2 years ago

vazirim commented 3 years ago

Using Alloy Analyzer 5.1.0 (Build Date: 2019-08-14T18:53:58.297Z), the following model causes the stack trace below.

one sig plan {
    planned_values: String -> RootModule
}

sig RootModule {
    resources: seq Resource
}

sig Resource {
    type: String,
    name: String,
    provider_name: String,
    values: String -> String
}

sig  Resource_planned_values_type {
    resources: set Vals_type
}

sig Vals_type {
    name: String,
    type: String,
    provider_name: String,
    attributes: String -> String

}

fun planned_values_fun[resource_name: String]: Resource_planned_values_type  {
    let vals = { v: Vals_type |  some r: Resource, i: String, j: Int  {
                            v.name = r.name
                            v.type = r.type 
                            v.provider_name = r.provider_name
                            v.attributes = r.values
                            r = i.(plan.planned_values).resources[j]
                        }
            } |
        {r: Resource_planned_values_type | r.resources = vals}
}

fun resources_map[]: Resource_planned_values_type {
    planned_values_fun["myresource"]

}

Stack trace:

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF
   387 vars. 96 primary vars. 626 clauses. 4ms.
   Writing the XML file...
Fatal error:
Error evaluating skolem $this/resources_map
StackTrace:
class edu.mit.csail.sdg.alloy4.ErrorFatal: Error evaluating skolem $this/resources_map
edu.mit.csail.sdg.translator.A4SolutionWriter.<init>(A4SolutionWriter.java:287)
edu.mit.csail.sdg.translator.A4SolutionWriter.writeInstance(A4SolutionWriter.java:302)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1667)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1650)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.writeXML(SimpleReporter.java:547)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.resultSAT(SimpleReporter.java:388)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1477)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:583)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:684)
edu.mit.csail.sdg.alloy4.WorkerEngine$5.run(WorkerEngine.java:468)
java.lang.Thread.run(Thread.java:748)
caused by...
class edu.mit.csail.sdg.alloy4.ErrorFatal: String literal "myresource" does not exist in this instance.

edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.visit(TranslateAlloyToKodkod.java:801)
edu.mit.csail.sdg.ast.ExprConstant.accept(ExprConstant.java:226)
edu.mit.csail.sdg.ast.VisitReturn.visitThis(VisitReturn.java:34)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.cset(TranslateAlloyToKodkod.java:690)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.visit(TranslateAlloyToKodkod.java:957)
edu.mit.csail.sdg.ast.ExprCall.accept(ExprCall.java:409)
edu.mit.csail.sdg.ast.VisitReturn.visitThis(VisitReturn.java:34)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.visit(TranslateAlloyToKodkod.java:832)
edu.mit.csail.sdg.ast.ExprUnary.accept(ExprUnary.java:485)
edu.mit.csail.sdg.ast.VisitReturn.visitThis(VisitReturn.java:34)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.visit(TranslateAlloyToKodkod.java:961)
edu.mit.csail.sdg.ast.ExprCall.accept(ExprCall.java:409)
edu.mit.csail.sdg.ast.VisitReturn.visitThis(VisitReturn.java:34)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.cset(TranslateAlloyToKodkod.java:690)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.visit(TranslateAlloyToKodkod.java:1175)
edu.mit.csail.sdg.ast.ExprBinary.accept(ExprBinary.java:734)
edu.mit.csail.sdg.ast.VisitReturn.visitThis(VisitReturn.java:34)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.alloy2kodkod(TranslateAlloyToKodkod.java:614)
edu.mit.csail.sdg.translator.A4Solution.eval(A4Solution.java:900)
edu.mit.csail.sdg.translator.A4SolutionWriter.writeExpr(A4SolutionWriter.java:102)
edu.mit.csail.sdg.translator.A4SolutionWriter.<init>(A4SolutionWriter.java:282)
edu.mit.csail.sdg.translator.A4SolutionWriter.writeInstance(A4SolutionWriter.java:302)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1667)
edu.mit.csail.sdg.translator.A4Solution.writeXML(A4Solution.java:1650)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.writeXML(SimpleReporter.java:547)
edu.mit.csail.sdg.alloy4whole.SimpleReporter.resultSAT(SimpleReporter.java:388)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1477)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:583)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:684)
edu.mit.csail.sdg.alloy4.WorkerEngine$5.run(WorkerEngine.java:468)
java.lang.Thread.run(Thread.java:748)
pkriens commented 2 years ago

We've had massive changes, could you verify and reopen if still the case?