Function vs operator behaviour in apalache

[agouglidis]

Hello all,

I'm running a simple specification using: APALACHE version: 0.29.1 | build: 146de56

and I'm getting a rather strange error.

The spec defines a mathematical function with Domain Nat |-> x^2 (not an operator) and I want to check an invariant.

------------------------------ MODULE Test ------------------------------
EXTENDS Naturals

VARIABLES
	\* @type: Int;
	posVal


Calc[x \in Nat] == x*x
                                            
Init == posVal \in (1..3) 

Next == posVal' = Calc[posVal]
              
Spec == /\ Init
        /\ [][Next]_posVal
        
Inv1 == posVal > 0
      
=============================================================================

When checking this, apalache finds an error since for some reason it does the following:

--------------------------- MODULE counterexample ----------------------------

EXTENDS Test

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 == posVal = 1

(* Transition 0 to State1 *)
State1 == posVal = 0

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == posVal <= 0

================================================================================

Not sure why tTransition 0 to State1 is: State1 == posVal = 0

Just wondering if this is a bug, or I'm missing how mathematical functions (not operators) are treated in apalache.

Note that:

• Using an operator instead of a mathematical function works correct (the invariant is not invalidated)
• The test spec doesn't raise the same issue in TLC (the error in TLC is obviously an overflow)

Thank you in advance,
AG

[shonfeder]

Hi @agouglidis. Thanks for raising the question. This does seem like strange behavior, so I'm gonna promote it into an issue so we can work it :)

[shonfeder]

@agouglidis: apparently our current approach is that functions with infinite domains are just not supported. We will be adding a validation pass to throw an error when this is encountered in the future.

For the time being, I think the fix for your case is to provide a bounded range for the domain of your function. E.g., something along these lines:

------------------------------ MODULE Test ------------------------------
EXTENDS Naturals

VARIABLES
	\* @type: Int;
	posVal


UpperBound == 100

Calc[x \in 1..UpperBound] == x*x

Init == posVal \in (1..3)

Next == posVal < UpperBound /\ posVal' = Calc[posVal]

Spec == /\ Init
        /\ [][Next]_posVal

Inv1 == posVal > 0
=============================================================================

[shonfeder]

See #2179 for the issue opened from this discussion.