Merge `updated_enabled_cdot`. #148

kape1395 · 2024-08-31T15:00:26Z

Here is an attempt to merge old branch updated_enabled_cdot.

Otherwise the already computed weights of an operator can rely on the arity of the operator before the dependence on parameters of the definition (`Foo(x) == INSTANCE Inner`) is added to the instantiated operator signature. Parametric instantiation changes the arity of operators, so the weights list needs to be recomputed, based on the arity after instantiation has been performed.

This change ensures that the testing commands are read after the closing horizontal rule (`=====*`) of the module. To do this, the nesting depth of submodules is tracked, by incrementing the counter `submodule_nesting_depth` when encountering a module opening (`-----*\s*MODULE`), and decrementing this counter when encountering a module closing (`=====*`). Commands are read after the module's end. Previously, commands were read after the first module closing (`=====*`), which results in errors in the presence of submodules.

"VARIABLES" otherwise.

that prints the names of modules in a module context.

When instantiating inside a LET, definitions are kept, and other module units omitted. A negative shift is applied to the remaining module units. This negative shift should equal minus the number of hypotheses that the omitted module unit introduces in the context. The number of hypotheses for each module unit is computed by the function `M_t.hyps_of_modunit`.

`Module.Elab` replaces each `INSTANCE` statement with definitions. If the instantiated module extends the module `TLAPS`, then the definitions include backend pragmas (constructor `Bpragma`).

…nstance

This change makes fingerprints take into account the result of the proof directive AutoUSE. Previously, fingerprinting was done before any expansion of definitions, normalization, and automated expansion of definitions, expansion of ENABLED and of \cdot. This approach worked correctly for BY DEF definitions, because those definitions were included in the fingerprint as context. With this change, only for proof obligations that include the proof directive AutoUSE, the fingerprint is computed after expansion of definitions, normalization, automated expansion of definitions, expansion of ENABLED, and of \cdot. This change ensures that the proof obligation is fingerprinted with all automatic expansions of definitions applied. A test is added that catches this error.

summary of changes - test fingerprints by running `tlapm` twice - add new proof directive `ENABLEDrules` - rewrite `ENABLEDaxioms` to remove the Boolean typeness assumptions - rewrite two proof rules that previously were in `ENABLEDaxioms` and now are in `ENABLEDrules`, to remove the Boolean typeness assumptions - correct soundness check for `ENABLEDrules` (previously for `ENABLEDaxioms`) - fingerprint the level correctness of proof obligations - revise renaming of variables in `ExpandENABLED` - removal of older implementation of `ENABLEDaxioms` - `ENABLEDaxioms` was not correctly collecting primed variables - use expression level in fingerprint of definition - record name of `Bpragma` in fingerprint - implement rewriting system for `ENABLEDrewrites` - add new proof directive `ENABLEDrewrites` - add test modules

These changes are for now kept as a separate commit, in case further rebasing is needed before preparing the pull request for the branch `update_enabled_cdot`.

… in ocaml 4.13

Signed-off-by: Karolis Petrauskas <[email protected]>

kape1395 · 2024-09-01T08:31:48Z

The LSP server currently fails with

LSP request failed with exception Not_found, backtrace:
Raised at Stdlib__List.find in file "list.ml", line 232, characters 10-25
Called from Tlapm_lib__Property.get in file "src/util/property.ml", line 71, characters 9-54
Called from Tlapm_lib__E_levels.get_level_info in file "src/expr/e_levels.ml" (inlined), line 68, characters 23-47
Called from Tlapm_lib__E_levels.get_level in file "src/expr/e_levels.ml", line 70, characters 21-37
Called from Tlapm_lib__Fingerprints.fp_sequent.spin in file "src/backend/fingerprints.ml", line 446, characters 23-48
Called from Tlapm_lib__Fingerprints.fp_sequent.spin in file "src/backend/fingerprints.ml", line 441, characters 13-26
...

It seems like the levels are not assigned somewhere.

Signed-off-by: Karolis Petrauskas <[email protected]>

kape1395 · 2024-09-01T21:14:04Z

@muenchnerkindl, @damiendoligez, who could review this PR?

Signed-off-by: Karolis Petrauskas <[email protected]>

damiendoligez

Looks good modulo a few suggestions.

damiendoligez · 2024-11-12T14:30:51Z

examples/EWD840.tla

 (***************************************************************************)
 Inv ==
  \/ P0:: \A i \in Nodes : tpos < i => ~ active[i]
  \/ P1:: \E j \in 0 .. tpos : color[j] = "black"
  \/ P2:: tcolor = "black"

-----------------------------------------------------------------------------
+USE NAssumption

 (* TypeOK is an inductive invariant *)


Suggested change

(* TypeOK is an inductive invariant *)

(* TypeCorrect is an inductive invariant *)

damiendoligez · 2024-11-12T14:39:42Z

lsp/lib/server/handlers.ml

@@ -351,7 +351,8 @@ module Make (CB : Callbacks) = struct
        with exc ->
          let open Jsonrpc.Response.Error in
          let exc_str = Printexc.to_string exc in
-          Eio.traceln "LSP request failed with exception %s" exc_str;
+          let exc_btr = Printexc.get_backtrace () in


It would be better to get the backtrace first, before Printexc.to_string has a chance to change it, so swap this line with the previous one.

damiendoligez · 2024-11-12T14:42:12Z

src/backend/fingerprints.ml

+            "Level<=1"
+        else
+            "Level>1"
+        end else "" in


Suggested change

end else "" in

end

else "" in

damiendoligez · 2024-11-12T14:51:14Z

src/backend/fpfile.ml

+  | ENABLEDrewrites
+  | ENABLEDrules


This change makes fingerprint files incompatible with previous versions of TLAPM, so we'll have to change the magic number. I've prepared a pull request on this pull request: #176

damiendoligez · 2024-11-12T15:43:34Z

src/expr/e_action.ml

+                            if (not (Hashtbl.mem primed_vars var_name)) then
+                                Hashtbl.add primed_vars var_name ()


Suggested change

if (not (Hashtbl.mem primed_vars var_name)) then

Hashtbl.add primed_vars var_name ()

Hashtbl.replace primed_vars var_name ()

johnyf and others added 30 commits March 31, 2021 14:24

BUG: lambdify ENABLED in operators with arguments

3c899a5

TST: add tests for ENABLED with INSTANCE

ab897dc

BUG: show "VARIABLE" for single variable,

8a5b74a

"VARIABLES" otherwise.

ENH: add function print_modules

c561dbe

that prints the names of modules in a module context.

BUG: load modules in EXTENDS of submodules

aa1f39b

REF: add details to error message

4d2129e

BUG: handle INSTANCE statements within LET

a4ca6ac

`Module.Elab` replaces each `INSTANCE` statement with definitions. If the instantiated module extends the module `TLAPS`, then the definitions include backend pragmas (constructor `Bpragma`).

REF: add details to error message

a5dc90a

BUG: fingerprint INSTANCE statements within LET

a87906f

`Module.Elab` replaces each `INSTANCE` statement with definitions. If the instantiated module extends the module `TLAPS`, then the definitions include backend pragmas (constructor `Bpragma`).

Merge branch 'let_instance_and_enabled_prm_instance' into merge_let_i…

93f5186

…nstance

liveness proof for EWD840 example

30f1415

fixed typo in Peterson example

017ebd8

DOC: add comments to example and tests

737dd12

TST: add TLA+ module LevelComparisonTest

f47164b

TST: add TLA+ module UnsoundCoalescingThmDecl_test

c7ff69d

BUG: correct soundness check for proof levels

426a200

DOC: add PlusCal-like algorithm for soundness check

aec7bbe

fixup! fpfile changes

70b4eaa

These changes are for now kept as a separate commit, in case further rebasing is needed before preparing the pull request for the branch `update_enabled_cdot`.

BUG: correct scoping in proof directive LevelComparison

6a4e5f8

API: print level comparison message only when verbose

23f6f0b

BUG: correct typo

c758c25

add labeled arguments in call of expand_enabled_cdot to avoid warning…

ee56b3d

… in ocaml 4.13

add example for simple liveness proof, contributed by Andreas Recke

a963bd3

Merge branch 'main' into updated_enabled_cdot

9c27e42

Signed-off-by: Karolis Petrauskas <[email protected]>

Print exception backtraces in LSP.

9a6cadd

Signed-off-by: Karolis Petrauskas <[email protected]>

kape1395 added 4 commits September 1, 2024 12:57

Proofs in examples/EWD840.tla fixed.

f002d24

Signed-off-by: Karolis Petrauskas <[email protected]>

Temporary workaround for making the LSP to work.

4f4344b

Signed-off-by: Karolis Petrauskas <[email protected]>

Fix proof in examples/SimpleMutex.tla.

cfacd96

Signed-off-by: Karolis Petrauskas <[email protected]>

Fix proof in examples/SimpleEventually.tla.

77ac33f

Signed-off-by: Karolis Petrauskas <[email protected]>

kape1395 self-assigned this Sep 1, 2024

Properly take the obligation fingerprints in the LSP.

7f63bdd

Signed-off-by: Karolis Petrauskas <[email protected]>

kape1395 marked this pull request as ready for review September 1, 2024 21:11

kape1395 mentioned this pull request Sep 3, 2024

Branch updated_enabled_cdot on top of dune, ocaml-5 and lsp. #95

Closed

Merge remote-tracking branch 'origin/main' into updated_enabled_cdot

b12dfff

Signed-off-by: Karolis Petrauskas <[email protected]>

damiendoligez requested changes Nov 26, 2024

View reviewed changes

damiendoligez mentioned this pull request Nov 26, 2024

change magic number for fingerprint files #176

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merge `updated_enabled_cdot`. #148

Merge `updated_enabled_cdot`. #148

kape1395 commented Aug 31, 2024

kape1395 commented Sep 1, 2024

kape1395 commented Sep 1, 2024

damiendoligez left a comment

damiendoligez Nov 12, 2024

damiendoligez Nov 12, 2024

damiendoligez Nov 12, 2024

damiendoligez Nov 12, 2024

damiendoligez Nov 12, 2024

	(* TypeOK is an inductive invariant *)
	(* TypeCorrect is an inductive invariant *)

		if (not (Hashtbl.mem primed_vars var_name)) then
		Hashtbl.add primed_vars var_name ()

	if (not (Hashtbl.mem primed_vars var_name)) then
	Hashtbl.add primed_vars var_name ()
	Hashtbl.replace primed_vars var_name ()

Merge updated_enabled_cdot. #148

Are you sure you want to change the base?

Merge updated_enabled_cdot. #148

Conversation

kape1395 commented Aug 31, 2024

kape1395 commented Sep 1, 2024

kape1395 commented Sep 1, 2024

damiendoligez left a comment

Choose a reason for hiding this comment

damiendoligez Nov 12, 2024

Choose a reason for hiding this comment

damiendoligez Nov 12, 2024

Choose a reason for hiding this comment

damiendoligez Nov 12, 2024

Choose a reason for hiding this comment

damiendoligez Nov 12, 2024

Choose a reason for hiding this comment

damiendoligez Nov 12, 2024

Choose a reason for hiding this comment

Merge `updated_enabled_cdot`. #148

Merge `updated_enabled_cdot`. #148