open NSPK + INV . ops p q : -> Prin . eq (p = q) = false . var N : Nonce var NS : NonceSet var C : Config -- red init(p q) =(1,*)=>* ((nonces: (N NS)) C) suchThat (not nonSec((nonces: (N NS)) C,N)) . -- -- Error: An allocation request for 128 bytes caused tenuring and a -- need for 262144 more bytes of heap. The operating system will not make -- the space available because the address space reserved for the heap -- could not be increased. -- [condition type: storage-condition] -- -- no counterexample is found red init(p q) =(1,3)=>* ((nonces: (N NS)) C) suchThat (not nonSec((nonces: (N NS)) C,N)) . -- infeasible red init(p q) =(1,4)=>* ((nonces: (N NS)) C) suchThat (not nonSec((nonces: (N NS)) C,N)) . close