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

Re: [tlaplus] Proving termination using the "will eventually be true" logic



Dear Stephan,

I found the "mistake". I used Ubuntu version 18.04 .... now I switched to version 22.04 and it compiled well. Common wisdom: update to the latest stable version before you dig into experimental packages.

But I found something else: when I compile the package (from the base folder) into the sandbox folder "/andreas/tlaprover", the resulting folders were
"bin" and "lib". Comparing the contents of this "lib/tlaps" folder with the contents of the "tlaps" folder generated by the bin-package I downloaded from http://tla.msr-inria.inria.fr/tlaps/content/Home.html,
there are some files missing. Such as isabelle and Z3 and so on.

I tried to solve it by putting both folders in correct order into the folder preferences of the TLA toolbox, but tlapm cannot find ls4 and Z3 etc. Could there be a gap in the compilation routine?

The TLAPS console shows
\* TLAPM version 1.5.0
\* launched at 2022-08-09 20:59:04 with command line:
\* /home/andreas/tlaprover/bin/tlapm --toolbox 29 34 --isaprove -I /home/andreas/Downloads/toolbox/CommunityModules-deps.jar -I /home/andreas/tlaprover/lib/tlaps/ -I /usr/local/lib/tlaps/ /home/andreas/.tlaplus/QueensPluscal/FinallyZero.tla
...
@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:34:11:34:13
@!!status:failed
@!!prover:ls4
@!!meth:time-limit: 10
@!!reason:Executable "ls4" not found in this PATH:
/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/usr/local/cuda/bin:/home/andreas/Downloads/tlapm-updated_enabled_cdot/bin:/home/andreas/Downloads/tlapm-updated_enabled_cdot/lib/tlaps/bin


It appears as if an old path setting (I cannot find that setting, but /home/andreas/Downloads/tlapm-updated_enabled_cdot/  is the folder I extracted the source files into). Where does
tlapm actually get its PATH (in red) from? Is there a config file I can edit? 

I would like to have both the common provers of the stable package and the ENABLEDrules from the experimental version.

I hope you can help me.

Kind regards
Andreas





Stephan Merz schrieb am Montag, 8. August 2022 um 14:23:01 UTC+2:
Arrghhh ... I checked, my OCaml version is called "4.11.1+default-unsafe-string" [1], and I dimly recall that I installed that version for compiling tlapm. 

If you are using opam, something like

opam switch create 4.11.1+default-unsafe-string

should install that version of the OCaml compiler, and

opam switch set ...

allows you to switch between different installed versions [2]. But since you say that 4.07.0 is the latest version, I gather that you installed OCaml using the default package manager of your OS, which may be behind what opam gives you.

Hope this helps,
Stephan

[1] https://opam.ocaml.org/packages/ocaml-variants/ocaml-variants.4.11.1+default-unsafe-string/
[2] https://opam.ocaml.org, in particular https://opam.ocaml.org/doc/man/opam-switch.html


On 5 Aug 2022, at 22:45, Andreas Recke <Andrea...@xxxxxxx> wrote:

Dear Stephan,

many thanks for your kind and helpful response. I downloaded the cdot-enabled branch to my computer and made an in-place installation.
I used the latest ocamlc version 4.07.0 which went nicely until it found an error that I think is not related to missing libraries (which should have popped up in the initial
source code section) but maybe a code error. Or do I just have an old library where StringSet.disjoint is not included?

"configure" did not report any error.

I hope you can help with this, too.

Best regards
Andreas



The compiler error message was:

cd `dirname expr/e_action.ml` \ 
&& ocamlopt -annot -g -warn-error +1+2+5+6+8+10..26+29..31+36  -I . -I backend -I frontend -I expr -I module -I proof -I util -I pars -I typesystem -I smt -I ../backend -I ../frontend -I ../expr -I ../module -I ../p
roof -I ../util -I ../pars -I ../typesystem -I ../smt -I .. -c `basename expr/e_action.ml` 
File "e_action.ml", line 1760, characters 27-45: 
Error: Unbound value StringSet.disjoint 
Makefile:140: recipe for target 'expr/e_action.cmx' failed 
make[1]: *** [expr/e_action.cmx] Error 2

This is the corresponding section (in red) in the source code

let group_conjuncts cx conjuncts =
    (* compute the primed variables of each conjunct *)
    let primed_variables = List.map (collect_primed_vars cx) conjuncts in
    (* return single group if any set of primed variables is `None` *)
    let has_none = List.exists
        (fun x -> match x with
            | None -> true
            | _ -> false) primed_variables in
    if has_none then
        [conjuncts]
    else
    begin
    (* split into minimal classes with disjoint sets of primed variables *)
    let primed_variables = List.map
        (fun x -> match x with
            | None -> assert false
            | Some x -> StringSet.of_seq (Stdlib.List.to_seq x)) primed_variables in
    let vars_conjuncts = List.map2 (fun a b -> (a, [b]))
        primed_variables conjuncts in
        (* (StringSet, expr list) list *)
    let groups: (StringSet.t * (E_t.expr list)) list ref = ref [] in
    let f (vars, es) =
        let (other, intersecting) = List.partition
            (fun (a, b) -> StringSet.disjoint a vars) !groups in
        let f (vars_a, es_a) (vars_b, es_b) =
            (StringSet.union vars_a vars_b, List.append es_a es_b) in
        let merged = List.fold_left f (vars, es) intersecting in
        groups := merged :: other in
    List.iter f vars_conjuncts;
    List.map (fun (vars, es) -> es) !groups
    end




Stephan Merz schrieb am Donnerstag, 4. August 2022 um 16:22:50 UTC+2:
Hello Andreas,

thank you for using TLAPS and for your question about termination proofs.

Let me first point out that the current distribution of TLAPS only supports proofs of safety properties. In particular, it has no support for reasoning about ENABLED, which in turn underlies the definition of fairness formulas, and the latter are a prerequisite for any proofs of liveness properties.

However, if you are brave enough to install a development version of TLAPS [1], below is a proof of the theorem you were after. As you found out, you cannot apply priming to arbitrary temporal formulas but only to state predicates. Also, as stated above, use of the fairness condition is important for this proof, and therefore it is useful to simplify the predicate ENABLED <<Next>>_vars and replace it by the simple state predicate i>0.

As you'll see, there are still a few rough edges in the proof, such as having to hide intermediate definitions before applying the induction rule, or inferring <1>3 from <1>2, which requires a mix of quantifier and temporal logic reasoning.

Nevertheless, I hope that this example will give you an overall idea of how to write liveness proofs.

Best regards,
Stephan

[1] The proof below was checked using the updated_enabled_cdot branch at https://github.com/tlaplus/tlapm/tree/updated_enabled_cdot, but I believe that the version at the master branch should also have worked.

---------------------------- MODULE FinallyZero ----------------------------
EXTENDS Integers, Naturals, TLC, TLAPS, NaturalsInduction

CONSTANTS N
ASSUME NAssumption == N \in Int /\ N > 0
VARIABLES i


vars == <<i>>

Init == i = N

Next == i > 0 /\ i' = i-1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Type Invariant 
TypeOk == i \in Int /\ i >= 0

\* Termination
Termination == i=0

\* Will terminate invariant
WillTerminate == <>(i=0)

\* Complete Invariant
(* not an invariant because it has a "<>" subformula *)

Inv == TypeOk /\ WillTerminate

(*
The formula is not level-correct, as SANY points out. You cannot prime
arbitrary temporal formulas in TLA, only state predicates.


THEOREM NextFinishes == ASSUME ~WillTerminate /\ Next => ~WillTerminate' PROVE FALSE
BY PTL DEF WillTerminate, Next
*)  

------------------------------------------------------------------------------
(* Proof of the algorithm. *)

(* Let's start by showing type correctness. *)
LEMMA Typing == Spec => []TypeOk
<1>1. Init => TypeOk
  BY NAssumption DEF Init, TypeOk
<1>2. TypeOk /\ [Next]_vars => TypeOk'
  BY DEF TypeOk, Next, vars
<1>. QED  BY <1>1, <1>2, PTL DEF Spec

(* Now let's rewrite the enabledness condition that occurs as part
   of the fairness hypothesis to a simple state predicate. *)
LEMMA EnabledNext ==
  ASSUME TypeOk
  PROVE  (ENABLED <<Next>>_vars) <=> i > 0
\* any Next step changes vars: here type correctness is relevant
<1>1. <<Next>>_vars <=> Next
  BY DEF TypeOk, Next, vars
\* therefore the ENABLED conditions are equivalent
<1>2. (ENABLED <<Next>>_vars) <=> ENABLED Next
  BY <1>1, ENABLEDrules
\* The method ExpandENABLED replaces ENABLED by explicit quantification.
<1>. QED
  BY <1>2, ExpandENABLED DEF Next, vars

(* We can now prove termination by induction. *)
THEOREM Terminate == Spec => <>Termination
<1>. DEFINE BSpec == []TypeOk /\ [][Next]_vars /\ WF_vars(Next)
            P(n) == [](i=n => <>Termination)
<1>1. SUFFICES  BSpec => <>Termination
  BY Typing, PTL DEF Spec
<1>2. BSpec => \A n \in Nat : P(n)
  <2>1. BSpec => P(0)
    <3>1. i=0 => Termination   BY DEF Termination
    <3>. QED                   BY <3>1, PTL
  <2>2. ASSUME NEW n \in Nat
        PROVE  (BSpec => P(n)) => (BSpec => P(n+1))
    <3>1. i=n+1 /\ [Next]_vars => (i=n+1)' \/ (i=n)'
      BY DEF Next, vars
    <3>2. i=n+1 /\ <<Next>>_vars => (i=n)'
      BY DEF Next, vars
    <3>3. TypeOk /\ i=n+1 => ENABLED <<Next>>_vars
      BY EnabledNext
    <3>4. BSpec => [](i=n+1 => <>(i=n))
      BY <3>1, <3>2, <3>3, PTL DEF BSpec
    <3>. QED  BY <3>4, PTL
  <2>. HIDE DEF BSpec, P
  <2>. QED  BY <2>1, <2>2, NatInduction
<1>3. BSpec => \A n \in Nat : i=n => <>Termination
  <2>. SUFFICES ASSUME NEW n \in Nat PROVE BSpec => (i=n => <>Termination)
    OBVIOUS
  <2>1. BSpec => P(n)    BY <1>2
  <2>. QED               BY <2>1, PTL
<1>4. BSpec => \E n \in Nat : i=n
  <2>1. TypeOk => \E n \in Nat : i=n    BY DEF TypeOk
  <2>. QED                              BY <2>1, PTL DEF BSpec
<1>. QED  BY <1>3, <1>4

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

On 4 Aug 2022, at 15:25, Andreas Recke <Andrea...@xxxxxxx> wrote:

Hi,

I am still a beginner with TLAPS andI am trying to prove  an algorithm which
works in TLC, but appears to be a bit more complicated to work on. So I decided
on a toy problem and found it very hard to prove. 

It is a simple algorithm that counts i from N to 0 and ends. 
I want to prove that it ends, i.e. WillTerminate == <>(i=0)

The logic of the proof is inductive and by contradiction:
1) show that Next is enabled for every i > 0
2) assume that a j \in Int exists for which WillTerminate is false
3) show that if 2 is true, then it will be true for j-1 
4) show that if 2 and 3 are true, then it will be true for j=0 which is a contradiction.

TLC toolbox dislikes when I something like
~WillTerminate /\ Next => (~WillTerminate)', because it contains action and temporal arguments.
So I am stuck.
Maybe TLAPS cannot work with the <> construct. 
An alternative is to set a "promise" that the algorithm ends to true and use this as
surrogate which never changes. But this appears to be incorrect.

I did not find anything how to work with this "will eventually be" temporal logic.

I would appreciate if someone has an idea or comment on this.

Kind regards
Andreas

P.S.: here is the spec



---------------------------- MODULE FinallyZero ----------------------------
EXTENDS Integers, Naturals, TLC, TLAPS

CONSTANTS N
ASSUME N > 0
VARIABLES i, expected_i

vars == <<i>>

Init == i = N /\ i \in Int /\ expected_i = 0

Next == i > 0 /\ i' = i-1 /\ UNCHANGED(expected_i)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Type Invariant 
TypeOk == i \in Int /\ i >= 0

\* Termination
Termination == i=0

\* Will terminate invariant
WillTerminate == <>(i=0)

\* Complete Invariant
Inv == TypeOk /\ WillTerminate

THEOREM NextFinishes == ASSUME ~WillTerminate /\ Next => ~WillTerminate' PROVE FALSE
BY PTL DEF WillTerminate, Next
  


=============================================================================
\* Modification History
\* Last modified Thu Aug 04 14:39:02 CEST 2022 by andreas
\* Created Sun Jul 31 21:38:42 CEST 2022 by andreas


-- 
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/eb93e2f8-57ae-4da1-aa52-3d878107773dn%40googlegroups.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+u...@xxxxxxxxxxxxxxxx.

--
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/cb0b33d7-4b3f-410f-bffa-aca13c4ead4an%40googlegroups.com.