From 6c641127d4b2d8da09e9d7796284c88c38702c14 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 10 Jan 2024 20:36:29 -0600 Subject: [PATCH 1/3] InvGen: Make modular argument truly mean modular analysis --- src/invgen/invGen.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/invgen/invGen.ml b/src/invgen/invGen.ml index 93be0c722..ccc0fbafb 100644 --- a/src/invgen/invGen.ml +++ b/src/invgen/invGen.ml @@ -836,8 +836,9 @@ let run_main eq_cond eq_main main two_state in_sys param sys = ) ( Flags.Invgen.top_only () ) ( - Flags.modular () |> not - ) two_state in_sys param sys + Flags.modular () + ) + two_state in_sys param sys |> ignore ; exit ExitCodes.success From 172b0ef2e0e4f87966c2fe6bb0a58d6a9e500a60 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 10 Jan 2024 20:47:40 -0600 Subject: [PATCH 2/3] InvGen: Always start generating invariants from the top --- src/invgen/invGen.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/invgen/invGen.ml b/src/invgen/invGen.ml index ccc0fbafb..e763c4991 100644 --- a/src/invgen/invGen.ml +++ b/src/invgen/invGen.ml @@ -722,7 +722,9 @@ module Make (Graph : GraphSig) : Out = struct ) (* If in modular mode, we already ran on the subsystems. Might as well start with the current top system since it's new. *) - |> ( if modular then identity else List.rev ) + (* Update: If in monolithic mode, also start with the current top system + since it is not clear that starting from the bottom really helps *) + (*|> ( if modular then identity else List.rev )*) |> function | [] -> KEvent.log L_info "%s no candidate to run on" (pref_s two_state) ; From 3f7874a23f87cf602a51c7376360379136578c2a Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 10 Jan 2024 20:51:19 -0600 Subject: [PATCH 3/3] Fix warning --- src/invgen/invGen.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/invgen/invGen.ml b/src/invgen/invGen.ml index e763c4991..91e2a4627 100644 --- a/src/invgen/invGen.ml +++ b/src/invgen/invGen.ml @@ -696,7 +696,7 @@ module Make (Graph : GraphSig) : Out = struct (** Invariant generation entry point. *) - let main max_depth top_only modular two_state input_sys aparam sys = + let main max_depth top_only _modular two_state input_sys aparam sys = try ( (* Format.printf "Starting (%b)@.@." two_state ; *)