Electrod/NuSMV as Solver -> unknown exception

[esb-dev]

Hi,

with the ring leader example from https://haslab.github.io/formal-software-design/protocol-design/index.html the following exception is thrown when checking "Check AtMostOneLeader for 5":

Unknown exception occurred: javax.xml.parsers.FactoryConfigurationError: Provider com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl not found

here a part of the stacktrace:

class edu.mit.csail.sdg.alloy4.ErrorFatal: Unknown exception occurred: javax.xml.parsers.FactoryConfigurationError: Provider com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl not found edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:622) edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742) edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485) java.lang.Thread.run(Thread.java:748)

Kind regards Burkhardt

[grayswandyr]

Thanks for the report! NuSMV crashes after 10+ min, probably due to lack of memory (nuXmv solves this in a matter of seconds). But this is badly reported by electrod. This needs a modification on the electrod side as well as on the Alloy side (I'll synchronize with @nmacedo for this). I'm filing issue https://github.com/grayswandyr/electrod/issues/6 on electrod.

EDIT: nonetheless, in the end, the outcome won't be better for the user as NuSMV doesn't say why it crashes.

[esb-dev]

I've in stalled nuXmv now and unfortunately I get the same exception.

[grayswandyr]

Which OS do you use? Do you get the exception in the GUI? Does the GUI crash? Could you please paste the exact model you're using and also tell which Options you're using? Thanks.

[esb-dev]

OS is Mac Monterey

The script is

open util/ordering[Node]

sig Node {
  succ : one Node,
  var inbox : set Node
}

fact {
  // at least one node
  some Node
}

fact {
  // succ forms a ring
  all n : Node | Node in n.^succ
}

fact {
  // initially inbox is empty
  no inbox
}

fun Elected : set Node {
  { n : Node | n not in n.inbox and once (n in n.inbox) }
}

pred initiate[n : Node] {
  // node n initiates the protocol

  historically n not in n.succ.inbox          // guard

  n.succ.inbox' = n.succ.inbox + n            // effect on n.succ.inbox
  all m : Node - n.succ | m.inbox' = m.inbox  // effect on the inboxes of other nodes
}

pred process[n : Node, i : Node] {
  // i is read and processed by node n

  i in n.inbox                                     // guard

  n.inbox' = n.inbox - i                           // effect on n.inbox
  gt[i,n] implies n.succ.inbox' = n.succ.inbox + i // effect on n.succ.inbox
          else    n.succ.inbox' = n.succ.inbox
  all m : Node - n.succ - n | m.inbox' = m.inbox   // effect on the inboxes of other nodes
}

pred stutter {
  inbox' = inbox
}

fact {
  // possible events
  always (
    stutter or
    some n : Node | initiate[n] or
    some n : Node, i : Node | process[n,i]
  )
}

run example {
  eventually some Elected
} for 3 Node

assert AtMostOneLeader {
  always (lone Elected)
}

check AtMostOneLeader for 5 // but 1.. steps

pred fairness {
  all n : Node, i : Node {
    (eventually always historically n not in n.succ.inbox) implies (always eventually initiate[n])
    (eventually always i in n.inbox)                       implies (always eventually process[n,i])
  }
}

assert AtLeastOneLeader {
  fairness implies eventually (some Elected)
}

check AtLeastOneLeader for 3 but 1.. steps

The GUI does not crash, is reports

Starting the solver...

   Forced to be exact: this/Node
Executing "Check AtMostOneLeader for 5"
   Sig ordering/Ord scope <= 1
   Sig this/Node scope <= 5
   Sig this/Node forced to have exactly 5 atoms.
   Sig this/Node == [[Node$0], [Node$1], [Node$2], [Node$3], [Node$4]]
   Sig ordering/Ord == [[ordering/Ord$0]]
   Generating facts...
   Simplifying the bounds...
   Solver=nuXmv Steps=1..10 Bitwidth=4 MaxSeq=5 SkolemDepth=4 Symmetry=20 Mode=batch
   Generating CNF...
   Generating the solution...
   No translation information available. 115ms.
   Solving...
A fatal error has occured: (see the stacktrace)
Unknown exception occurred:
javax.xml.parsers.FactoryConfigurationError: Provider
com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl
not found

stacktrace is

class edu.mit.csail.sdg.alloy4.ErrorFatal: Unknown exception occurred: javax.xml.parsers.FactoryConfigurationError: Provider com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl not found
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:622)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742)
edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485)
java.lang.Thread.run(Thread.java:748)
caused by...
class javax.xml.parsers.FactoryConfigurationError: Provider com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl not found
javax.xml.parsers.FactoryFinder.newInstance(FactoryFinder.java:200)
javax.xml.parsers.FactoryFinder.newInstance(FactoryFinder.java:152)
javax.xml.parsers.FactoryFinder.find(FactoryFinder.java:277)
javax.xml.parsers.DocumentBuilderFactory.newInstance(DocumentBuilderFactory.java:120)
kodkod.engine.unbounded.ElectrodReader.read(ElectrodReader.java:88)
kodkod.engine.ElectrodSolver.go(ElectrodSolver.java:294)
kodkod.engine.ElectrodSolver.solve(ElectrodSolver.java:102)
kodkod.engine.ElectrodSolver.solve(ElectrodSolver.java:72)
kodkod.engine.PardinusSolver.solveAll(PardinusSolver.java:240)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1681)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:610)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742)
edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485)
java.lang.Thread.run(Thread.java:748)
caused by...
class java.lang.ClassNotFoundException: com/sun/org/apache/xerces/internal/jaxp/DocumentBuilderFactoryImpl
java.lang.Class.forName0(Native Method)
java.lang.Class.forName(Class.java:348)
javax.xml.parsers.FactoryFinder.getProviderClass(FactoryFinder.java:124)
javax.xml.parsers.FactoryFinder.newInstance(FactoryFinder.java:188)
javax.xml.parsers.FactoryFinder.newInstance(FactoryFinder.java:152)
javax.xml.parsers.FactoryFinder.find(FactoryFinder.java:277)
javax.xml.parsers.DocumentBuilderFactory.newInstance(DocumentBuilderFactory.java:120)
kodkod.engine.unbounded.ElectrodReader.read(ElectrodReader.java:88)
kodkod.engine.ElectrodSolver.go(ElectrodSolver.java:294)
kodkod.engine.ElectrodSolver.solve(ElectrodSolver.java:102)
kodkod.engine.ElectrodSolver.solve(ElectrodSolver.java:72)
kodkod.engine.PardinusSolver.solveAll(PardinusSolver.java:240)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1681)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:610)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:742)
edu.mit.csail.sdg.alloy4.WorkerEngine$6.run(WorkerEngine.java:485)
java.lang.Thread.run(Thread.java:748)

[grayswandyr]

OK so I'm on GNU/Linux and can't reproduce the bug, nuXmv runs flawlessly in a couple of seconds. I suppose it's OS-dependent. The issue I had run into and talked about before isn't related to this. @nmacedo can you reproduce it? do you use Xerces to parse the XML output of electrod?

[esb-dev]

Hi,

I played a bit with the Alloy 6 App. If I open the package content in the finder and start org.alloytools.alloy.dist.jar directly, i.e. not the App but just the jar, then nuXMV and NuSMV are doing fine. It seems to be a problem with the packaging into the Mac App.

-- Burkhardt

[pkriens]

This is caused by the packager. We're missing some packages in the jvm

We need to use the jpackager from Java 17

[grayswandyr]

@pkriens can you handle this for 6.2?

[pkriens]

@grayswandyr this will be handled. I intend to make packages for all OS's/architectures using the new Java 17 and later support. This will fix this problem I think.

[pkriens]

A lot of work done to make the solvers work. This should work now