X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=01fa63961763022f2bba37c4807abc3813dbb40b;hp=9fe128ae92a27b9b6883ae46bb5205e8b50994f3;hb=acd23a33d837d03c813212ec3896a86edef16e87;hpb=ff57c96ae37629bfd6ca7695653ac02b4ac013e9 diff --git a/src/ata.ml b/src/ata.ml index 9fe128a..01fa639 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -199,6 +199,8 @@ type config = { unsat : StateSet.t; todo : TransList.t; summary : node_summary; + (** optimization infos, + not taken into account during hashconsing *) mutable round : int; } @@ -240,7 +242,7 @@ let dummy_config = Config.make { sat = StateSet.empty; unsat = StateSet.empty; todo = TransList.nil; summary = dummy_summary; - round = 0 + round = 0; } @@ -442,7 +444,7 @@ let eval_trans auto fcs nss ps ss = let unsat = StateSet.union unsat (StateSet.diff removed kept) in (* States that were found once to be satisfiable remain so *) let unsat = StateSet.diff unsat sat in - let new_config = Config.make { sat; unsat; todo ; summary = old_summary ; round = 0 } in + let new_config = Config.make { old_config.Config.node with sat; unsat; todo; } in Cache.N4.add auto.cache4 oid fcsid nssid psid new_config; new_config in