Re: [tlaplus] Using a Division Operator with TLAPS

On Wed, Dec 4, 2019 at 5:47 PM <hjh2bs@xxxxxx> wrote:

Hi,

I'm working on proving an algorithm using TLAPS that requires dividing integers by two. I understand there's no support for real numbers/division in the backend provers, so I am using an operator:

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

The problem I'm running into is when trying to prove properties using the above operator with set expressions. The following example demonstrates this:

EXTENDS Integers, TLAPS, FiniteSets divide_by_two(n) == CHOOSE k \in Nat: n=2*k CONSTANTS N VARIABLES x Init == x = divide_by_two(N) PositiveInvariant == x >= 0 ASSUME NumberAssumption == N \in {2,4,6,8,10} THEOREM PositiveDivisionProperty == Init => PositiveInvariant <1> SUFFICES ASSUME Init PROVE PositiveInvariant OBVIOUS <1> QED BY NumberAssumption DEF Init, PositiveInvariant, divide_by_two

The backend provers are unable to prove the above theorem. SMT specifically times out and increasing the timeout doesn't appear to help.

Changing the assumption to:

ASSUME NumberAssumption == N = 10

will successfully prove the theorem. Are the backend provers able to work with 'CHOOSE' _expression_ in conjunction with sets? Is there anything wrong with how I'm specifying the assumption? The actual algorithm will require using the division operator with a few 'min'/'max' operators, which may also complicate the proof process, so I'm wondering if TLAPS is able to prove these sort of algorithms that require arithmetic.

Best,
Hans

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5d12aa41-9036-4ba4-856a-bf5070853122%40googlegroups.com.