From 578eda0462b67e5a5472df4bc648dfe8458f1ed2 Mon Sep 17 00:00:00 2001 From: David Chemouil Date: Thu, 23 May 2024 14:51:10 +0200 Subject: [PATCH 1/4] fix pp typo; fix wrong arity handling for join --- src/Raw_to_ast.ml | 28 +++++++++++++--------------- src/Smv.ml | 2 +- 2 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/Raw_to_ast.ml b/src/Raw_to_ast.ml index 155d961..7857b56 100644 --- a/src/Raw_to_ast.ml +++ b/src/Raw_to_ast.ml @@ -519,14 +519,6 @@ let refine_identifiers unseen_shifts raw_pb = * Check arities *******************************************************************************) -(* computes the arity of a join *) -let join_arity ar1 ar2 = - match (ar1, ar2) with - | Some a1, Some a2 -> - let res = a1 + a2 - 2 in - if res > 0 then Some res else None - | Some _, None | None, Some _ | None, None -> None - let str_exp = Fmtc.to_to_string (Fmtc.hbox2 Ast.pp_exp) let compute_arities elo = @@ -675,13 +667,19 @@ let compute_arities elo = let ar = Some (a1 + a2) in return_exp exp ar @@ rbinary e1' op e2' | None, _ | _, None -> return_exp exp None @@ rbinary e1' op e2') - | Join -> - let ar_join = join_arity ar1 ar2 in - if Option.is_none ar_join then - Result.fail - @@ Fmtc.str "wrong arities for the dot join of %s and %s" - (str_exp e1') (str_exp e2') - else return_exp exp ar_join @@ rbinary e1' op e2') + | Join -> ( + match (ar1, ar2) with + | Some _, None | None, Some _ | None, None -> + return_exp exp None @@ rbinary e1' op e2' + | Some a1, Some a2 -> + let res = a1 + a2 - 2 in + if res < 0 then + Result.fail + @@ Fmtc.str "wrong arities for the dot join of %s and %s" + (str_exp e1') (str_exp e2') + else + return_exp exp (if res > 0 then Some res else None) + @@ rbinary e1' op e2')) | RIte (c, t, e) -> ( let c' = walk_fml ctx c in let t' = walk_exp ctx t in diff --git a/src/Smv.ml b/src/Smv.ml index 36956c8..460de09 100644 --- a/src/Smv.ml +++ b/src/Smv.ml @@ -476,7 +476,7 @@ module Make_SMV_file_format (Ltl : Solver.LTL) : pf out "%s@\n" elo_str; stratified_fml |> List.iter - (pf out "TRANS@\n[%a@];@\n@\n" + (pf out "TRANS@\n@[%a@];@\n@\n" (Ltl.pp_gather_variables ~next_is_X:false bitwidth auxiliaries variables))) trans; From 2e84c680096874eaf7580fc497eb5337d83cd625 Mon Sep 17 00:00:00 2001 From: David Chemouil Date: Fri, 24 May 2024 11:32:32 +0200 Subject: [PATCH 2/4] fix parsing error or interger if/then/else --- src/Elo_recursor.ml | 1 - src/Parser.mly | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Elo_recursor.ml b/src/Elo_recursor.ml index 06a5d02..29567b1 100644 --- a/src/Elo_recursor.ml +++ b/src/Elo_recursor.ml @@ -91,7 +91,6 @@ class virtual ['self] recursor = method virtual build_X : _ method virtual build_oexp : _ method virtual build_Zershift : _ - method virtual build_Sum : _ method virtual build_Sershift : _ method virtual build_Rem : _ method virtual build_Mul : _ diff --git a/src/Parser.mly b/src/Parser.mly index 0b2fae9..b9c603d 100644 --- a/src/Parser.mly +++ b/src/Parser.mly @@ -496,8 +496,8 @@ iexpr: | HASH e = expr { G.iexp (Location.from_positions $startpos $endpos) @@ G.card e } -| formula IIMPLIES iexpr IELSE iexpr { G.iexp (Location.from_positions $startpos $endpos) - @@ G.num 0 } +| c = formula IIMPLIES t = iexpr IELSE e = iexpr { G.iexp (Location.from_positions $startpos $endpos) + @@ G.ifthenelse_arith c t e } | SMALLINT e = brackets(expr) { G.iexp (Location.from_positions $startpos $endpos) @@ G.small_int e } From e49dfb6884afd22f8d034f2f0b0cde2cfd475e60 Mon Sep 17 00:00:00 2001 From: Julien Brunel Date: Fri, 24 May 2024 11:40:51 +0200 Subject: [PATCH 3/4] Invar_computation handling of integer ifthenelse --- src/Invar_computation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Invar_computation.ml b/src/Invar_computation.ml index fa5abc4..7c3b9a9 100644 --- a/src/Invar_computation.ml +++ b/src/Invar_computation.ml @@ -219,7 +219,7 @@ class ['self] computer (elo : Elo.t) = method build_Lshift () = max_color_wiwt method build_Div () = max_color_wiwt method build_Big_int () = Fun.id - method build_AIte () = failwith ("TODO" ^ __LOC__) + method build_AIte () = fun cond_color _ _ -> cond_color end (* Computes the color (Invar, Static_prop, Init or Temporal) of an From 7b93762e50c4f4433f8d3c3cd56d506d2fc2a74f Mon Sep 17 00:00:00 2001 From: David Chemouil Date: Fri, 24 May 2024 16:17:39 +0200 Subject: [PATCH 4/4] add test case for int i/t/e --- src/Invar_computation.ml | 2 +- test/test_aite.elo | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 test/test_aite.elo diff --git a/src/Invar_computation.ml b/src/Invar_computation.ml index 7c3b9a9..93cd1c3 100644 --- a/src/Invar_computation.ml +++ b/src/Invar_computation.ml @@ -219,7 +219,7 @@ class ['self] computer (elo : Elo.t) = method build_Lshift () = max_color_wiwt method build_Div () = max_color_wiwt method build_Big_int () = Fun.id - method build_AIte () = fun cond_color _ _ -> cond_color + method build_AIte () cond_color _ _ = cond_color end (* Computes the color (Invar, Static_prop, Init or Temporal) of an diff --git a/test/test_aite.elo b/test/test_aite.elo new file mode 100644 index 0000000..e38ebe1 --- /dev/null +++ b/test/test_aite.elo @@ -0,0 +1,17 @@ +univ : { A#0 A#1 A#2 -4 -3 -2 -1 0 1 2 3 }; + +const Int##min :1 { ( -4 ) }; +const Int##zero :1 { ( 0 ) }; +const Int##max :1 { ( 3 ) }; +const Int##next :2 { ( -4 -3 ) ( -3 -2 ) ( -2 -1 ) ( -1 0 ) ( 0 1 ) ( 1 2 ) ( 2 3 ) }; +const seq##Int :1 { ( 0 ) ( 1 ) ( 2 ) }; +const String :1 { }; +const this##A :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) }; +var this##B :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) }; +var this##C :1 { } { ( A#0 ) ( A#1 ) ( A#2 ) }; +const ints :1 { ( -4 ) ( -3 ) ( -2 ) ( -1 ) ( 0 ) ( 1 ) ( 2 ) ( 3 ) }; + +run +((this##B = this##C) iimplies + (#(this##B)) ielse + (#((ints + String) + this##A))) < (2);