From 63e090633cf7f2d53eb618f0df4eb5e8837fdd6d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Tue, 23 May 2017 10:56:50 +0200 Subject: [PATCH] Corrected bug in causality analysis The following node was accepted by the causality analysis: node m(x:int) = (y,z:int) let automaton state A do y = x + z; z = x + 1; until x = 3 then B state B do y = x + 3; z = y * x; until x = 10 then A end tel Each state is indeed causal, but once the automaton is translated to equations (which is the systematic way in the current version), the node is not schedulable. Correction: all "Or" of dependency constraints translated to "And". This constraint could be relaxed if code generation is done from Heptagon code, before translation to minils equations. --- compiler/heptagon/analysis/causality.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index b6e0845..3599e9e 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -203,12 +203,12 @@ and typing_eq eq = and typing_switch handlers = let handler { w_block = b } = typing_block b in - corlist (List.map handler handlers) + candlist (List.map handler handlers) and typing_present handlers b = let handler { p_cond = e; p_block = b } = cseq (typing e) (typing_block b) in - corlist ((typing_block b) :: (List.map handler handlers)) + candlist ((typing_block b) :: (List.map handler handlers)) and typing_automaton state_handlers = (* typing the body of the automaton *) @@ -222,7 +222,7 @@ and typing_automaton state_handlers = let t2 = candlist (List.map escape sunless) in cseq t2 (cseq tb t1) in - corlist (List.map handler state_handlers) + candlist (List.map handler state_handlers) and typing_block { b_local = _dec; b_equs = eq_list; b_loc = _loc } = (*let teq = typing_eqs eq_list in @@ -247,8 +247,8 @@ let typing_contract loc contract = ((typing e_a) :: (typing e_a_loc) :: (typing e_g_loc) :: - (List.map (fun o -> typing o.o_exp) objs) - )) in + (List.map (fun o -> typing o.o_exp) objs) + )) in Causal.check loc t_contract; let t_contract = clear (build b.b_local) t_contract in t_contract