marcellussiegburg / call-alloy

MIT License
3 stars 2 forks source link

call-alloy-0.4.1 testsuite failing for Stackage LTS #14

Closed juhp closed 8 months ago

juhp commented 8 months ago

FYI

           Failed parsing the Alloy code?:                                                                               [98/925911]

           abstract sig Node {                                                                                                      
             flow : Node -> lone Int,                                                                                               
             stored : one Int                                                                                                       
           } {                                                                                                                      
             stored >= 0                                                                                                            
             all n : Node | some flow[n] implies flow[n] >= 0                                                                       
             no flow[this]                                                                                                          
           }                                                                                                                        

           fun currentFlow(x, y : one Node) : Int {                                                                                 
             let s = x.stored, f = x.flow[y] | s < f implies s else f                                                               
           }                                                                                                                        

           pred withFlow[x, y : one Node] {                                                                                         
             currentFlow[x, y] > 0                                                                                                  
           }                                                                                                                        

           run withFlow for 2 Int, 2 Node                                                                                           

               using solver PLingeling generates an instance [✘]                                                                    
               using solver SAT4J generates an instance [✔]                                                                         
               called in parallel does not create issues [✔]                                                                        
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:280: hPu
tChar: illegal operation (handle is closed)                                                                                         
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:282: hPu
tChar: illegal operation (handle is closed)                                                                                         
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:280: hPu
tChar: illegal operation (handle is closed)                       
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:282: hPu
tChar: resource vanished (Broken pipe)                            
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:280: hPu
tChar: resource vanished (Broken pipe)                            
           Warning: Maybe not complete instance was sent to Alloy (Are timeouts set? Make sure they are not too small!): fd:282: hPu
tChar: illegal operation (handle is closed)                       
               called in parallel using too low timeout returns no instances [✔]

           Failures:                                                                                                     [60/925911]

             test/Language/Alloy/CallSpec.hs:46:7: 
             1) Language.Alloy.Call.getInstances using solver MiniSat generates an instance
                  uncaught exception: IOException of type UserError
                  user error (Exception in thread "main" Fatal error:
                  The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: 'long kodkod.engine.satlab.MiniSat.make(
)'                               
                        at edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:566)     
                        at alloy.RunAlloy.runAlloy(RunAlloy.java:109)
                        at alloy.RunAlloy.main(RunAlloy.java:60)
                  Caused by: java.lang.UnsatisfiedLinkError: 'long kodkod.engine.satlab.MiniSat.make()'
                        at kodkod.engine.satlab.MiniSat.make(Native Method)
                        at kodkod.engine.satlab.MiniSat.<init>(MiniSat.java:35)
                        at kodkod.engine.satlab.SATFactory$5.instance(SATFactory.java:131)
                        at kodkod.engine.fol2sat.Bool2CNFTranslator.translate(Bool2CNFTranslator.java:67)
                        at kodkod.engine.fol2sat.Translator.toCNF(Translator.java:654)
                        at kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:623)
                        at kodkod.engine.fol2sat.Translator.translate(Translator.java:467)
                        at kodkod.engine.fol2sat.Translator.translate(Translator.java:156)
                        at kodkod.engine.ExtendedSolver$SolutionIterator.<init>(ExtendedSolver.java:111)
                        at kodkod.engine.ExtendedSolver.iterator(ExtendedSolver.java:324)
                        at kodkod.engine.AbstractKodkodSolver.solveAll(AbstractKodkodSolver.java:182)
                        at kodkod.engine.PardinusSolver.solveAll(PardinusSolver.java:196)
                        at edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1681)
                        at edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:564)     
                        ... 2 more
                  )

             To rerun use: --match "/Language.Alloy.Call/getInstances/using solver MiniSat generates an instance/" --seed 1483564492

             test/Language/Alloy/CallSpec.hs:46:7:                                                                       [29/925911]
             2) Language.Alloy.Call.getInstances using solver PLingeling generates an instance
                  uncaught exception: IOException of type UserError
                  user error (Exception in thread "main" Fatal error:
                  Unknown exception occurred: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOEx
ception: Cannot run program "plingeling": error=2, No such file or directory                                                        
                        at edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:576)     
                        at alloy.RunAlloy.runAlloy(RunAlloy.java:109)
                        at alloy.RunAlloy.main(RunAlloy.java:60)
                  Caused by: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot r
un program "plingeling": error=2, No such file or directory       
                        at kodkod.engine.AbstractKodkodSolver.solve(AbstractKodkodSolver.java:147)
                        at kodkod.engine.PardinusSolver.solve(PardinusSolver.java:180)
                        at edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1672)
                        at edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:564)     
                        ... 2 more
                  Caused by: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2
, No such file or directory      
                        at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:257)
                        at kodkod.engine.AbstractKodkodSolver.solve(AbstractKodkodSolver.java:140)
                        ... 5 more
                  Caused by: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory
                        at java.base/java.lang.ProcessBuilder.start(ProcessBuilder.java:1128)
                        at java.base/java.lang.ProcessBuilder.start(ProcessBuilder.java:1071)
                        at java.base/java.lang.Runtime.exec(Runtime.java:592)
                        at java.base/java.lang.Runtime.exec(Runtime.java:451)
                        at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:219)
                        ... 6 more
                  Caused by: java.io.IOException: error=2, No such file or directory
                        at java.base/java.lang.ProcessImpl.forkAndExec(Native Method)
                        at java.base/java.lang.ProcessImpl.<init>(ProcessImpl.java:340)
                        at java.base/java.lang.ProcessImpl.start(ProcessImpl.java:271)
                        at java.base/java.lang.ProcessBuilder.start(ProcessBuilder.java:1107)
                        ... 10 more
                  )

             To rerun use: --match "/Language.Alloy.Call/getInstances/using solver PLingeling generates an instance/" --seed 1483564
492                              

           Randomized with seed 1483564492
marcellussiegburg commented 8 months ago

Thanks for the heads up. I guess there are some Java?-Dependencies missing. However I do not know how to reproduce this. When I perform:

stack unpack "call-alloy-0.4.1"
cd "call-alloy-0.4.1"
rm -f stack.yaml
stack init --resolver "lts-22.6" --ignore-subdirs
stack build --resolver "lts-22.6" --haddock --test --bench --no-run-benchmarks

I get no issues. I guess I have to publish a new release disabling some of the tests.

juhp commented 8 months ago

Yea looks that way

I forgot to reference this issue in the lts-haskell commit where I allowed the failure

marcellussiegburg commented 8 months ago

The latest release (c6f5b873391b9b514d8aab7c9839d292e3e97805) published on hackage should resolve the issue.