[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Hans He <hjh2bs@xxxxxx>*Date*: Wed, 4 Dec 2019 22:33:05 -0500*References*: <5d12aa41-9036-4ba4-856a-bf5070853122@googlegroups.com> <CAJSuO-_Wo9UhL3_Di9NpLO+SDLj-tuSNbLoSPObjwP_-JMKpyQ@mail.gmail.com>

I'm able to use the above operator with Z3. Thank you for your help.

Hans

On Wed, Dec 4, 2019 at 6:02 PM Saksham Chand <schand@xxxxxxxxxxxxxxxxx> wrote:

The following should work and invoke Z3:divide_by_two(n) == n \div 2--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*kThe 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, FiniteSetsdivide_by_two(n) == CHOOSE k \in Nat: n=2*kCONSTANTS NVARIABLES xInit == x = divide_by_two(N)PositiveInvariant == x >= 0ASSUME NumberAssumption == N \in {2,4,6,8,10}THEOREM PositiveDivisionProperty == Init => PositiveInvariant<1> SUFFICES ASSUME InitPROVE PositiveInvariantOBVIOUS<1> QEDBY 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.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NLLfoXEvxCU/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-_Wo9UhL3_Di9NpLO%2BSDLj-tuSNbLoSPObjwP_-JMKpyQ%40mail.gmail.com.

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/CACOXEhA-Z-DrYi-rjdd6o0D%2BgGLe9YBZ4-TPUf%2BF%3Dy175-10uQ%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] Using a Division Operator with TLAPS***From:*Stephan Merz

**References**:**[tlaplus] Using a Division Operator with TLAPS***From:*hjh2bs

**Re: [tlaplus] Using a Division Operator with TLAPS***From:*Saksham Chand

- Prev by Date:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Next by Date:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Previous by thread:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Next by thread:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Index(es):