Fatal error occurs when using nuSMV or nuXmv, NullPointerException with CryptoMiniSat

[Joshua27]

Hi, I use Alloy 6 and the Alloy Analyzer 6.1.0 on Ubuntu 22.04 to check the following model:

enum colors {blue,green,yellow}

one sig population {
  var chameleons: colors -> one Int
}

fact init {
  (population.chameleons)[blue] = 13 and 
  (population.chameleons)[green] = 15 and 
  (population.chameleons)[yellow] = 17
}

pred meet[c1: colors, c2: colors] {
  c1 != c2 and (population.chameleons)[c1] > 0 and (population.chameleons)[c2] > 0 and 
  (let c3 = ((colors - c1) - c2) | 
         population.chameleons' =                      
            (((population.chameleons 
               ++ (c1->(minus[(population.chameleons)[c1],1]))) 
               ++ (c2->(minus[(population.chameleons)[c2],1]))) 
               ++ (c3->(plus[(population.chameleons)[c3],2]))
           ))
}

pred skip { 
  population.chameleons' = population.chameleons
}

fact step {
  always ((some c1,c2: colors | meet[c1,c2]) or skip)
}

pred invariant {
  eventually ((population.chameleons)[blue] = 0 and (population.chameleons)[green] = 0)
}

run invariant for 7 Int, 361 steps

When using nuSMV or nuXmv, the following fatal error occurs:

Invalid specification for complete backend.
Invalid formula: ((this/blue . this/population.chameleons) =
Int[13])

When using CryptoMiniSat, a NullPointerException occurs: Unknown exception occurred: java.lang.NullPointerException

The other constraint solvers work but they are not able to check the model in a reasonable amount of time.

Best regards, Joshua

[grayswandyr]

Unfortunately, as of now, the translation to SMV solvers does not handle integers. We hope/expect to be able to release a new version in 2023, which will handle specs fetauring integers

In any case, I don't think the whole framework could handle a trace as long as this one. Fortunately, if you want to check an invariant, you can get rid of temporal logic and long traces by just checking the invariant on every event (and on the initial state). Hope this helps.

[Joshua27]

Ok, I didn't know that. Thanks for the quick reply.

[grayswandyr]

Tracked in #197 .