Extremely slow clock bounds computation

[osankur]

The following model is a straight-line automaton with 100 states and 2 clocks. But the clock bounds computation takes about 40s. This seems to increase quickly with the size of the model.

system:bug
clock:1:x
clock:1:y

event:a
process:P
location:P:l0{initial:}
location:P:l1{}
location:P:l2{}
location:P:l3{}
location:P:l4{}
location:P:l5{}
location:P:l6{}
location:P:l7{}
location:P:l8{}
location:P:l9{}
location:P:l10{}
location:P:l11{}
location:P:l12{}
location:P:l13{}
location:P:l14{}
location:P:l15{}
location:P:l16{}
location:P:l17{}
location:P:l18{}
location:P:l19{}
location:P:l20{}
location:P:l21{}
location:P:l22{}
location:P:l23{}
location:P:l24{}
location:P:l25{}
location:P:l26{}
location:P:l27{}
location:P:l28{}
location:P:l29{}
location:P:l30{}
location:P:l31{}
location:P:l32{}
location:P:l33{}
location:P:l34{}
location:P:l35{}
location:P:l36{}
location:P:l37{}
location:P:l38{}
location:P:l39{}
location:P:l40{}
location:P:l41{}
location:P:l42{}
location:P:l43{}
location:P:l44{}
location:P:l45{}
location:P:l46{}
location:P:l47{}
location:P:l48{}
location:P:l49{}
location:P:l50{}
location:P:l51{}
location:P:l52{}
location:P:l53{}
location:P:l54{}
location:P:l55{}
location:P:l56{}
location:P:l57{}
location:P:l58{}
location:P:l59{}
location:P:l60{}
location:P:l61{}
location:P:l62{}
location:P:l63{}
location:P:l64{}
location:P:l65{}
location:P:l66{}
location:P:l67{}
location:P:l68{}
location:P:l69{}
location:P:l70{}
location:P:l71{}
location:P:l72{}
location:P:l73{}
location:P:l74{}
location:P:l75{}
location:P:l76{}
location:P:l77{}
location:P:l78{}
location:P:l79{}
location:P:l80{}
location:P:l81{}
location:P:l82{}
location:P:l83{}
location:P:l84{}
location:P:l85{}
location:P:l86{}
location:P:l87{}
location:P:l88{}
location:P:l89{}
location:P:l90{}
location:P:l91{}
location:P:l92{}
location:P:l93{}
location:P:l94{}
location:P:l95{}
location:P:l96{}
location:P:l97{}
location:P:l98{}
location:P:l99{}
edge:P:l0:l1:a{provided: y>0 && x <1: do : x=0}
edge:P:l1:l2:a{provided: y>0 && x <1: do : x=0}
edge:P:l2:l3:a{provided: y>0 && x <1: do : x=0}
edge:P:l3:l4:a{provided: y>0 && x <1: do : x=0}
edge:P:l4:l5:a{provided: y>0 && x <1: do : x=0}
edge:P:l5:l6:a{provided: y>0 && x <1: do : x=0}
edge:P:l6:l7:a{provided: y>0 && x <1: do : x=0}
edge:P:l7:l8:a{provided: y>0 && x <1: do : x=0}
edge:P:l8:l9:a{provided: y>0 && x <1: do : x=0}
edge:P:l9:l10:a{provided: y>0 && x <1: do : x=0}
edge:P:l10:l11:a{provided: y>0 && x <1: do : x=0}
edge:P:l11:l12:a{provided: y>0 && x <1: do : x=0}
edge:P:l12:l13:a{provided: y>0 && x <1: do : x=0}
edge:P:l13:l14:a{provided: y>0 && x <1: do : x=0}
edge:P:l14:l15:a{provided: y>0 && x <1: do : x=0}
edge:P:l15:l16:a{provided: y>0 && x <1: do : x=0}
edge:P:l16:l17:a{provided: y>0 && x <1: do : x=0}
edge:P:l17:l18:a{provided: y>0 && x <1: do : x=0}
edge:P:l18:l19:a{provided: y>0 && x <1: do : x=0}
edge:P:l19:l20:a{provided: y>0 && x <1: do : x=0}
edge:P:l20:l21:a{provided: y>0 && x <1: do : x=0}
edge:P:l21:l22:a{provided: y>0 && x <1: do : x=0}
edge:P:l22:l23:a{provided: y>0 && x <1: do : x=0}
edge:P:l23:l24:a{provided: y>0 && x <1: do : x=0}
edge:P:l24:l25:a{provided: y>0 && x <1: do : x=0}
edge:P:l25:l26:a{provided: y>0 && x <1: do : x=0}
edge:P:l26:l27:a{provided: y>0 && x <1: do : x=0}
edge:P:l27:l28:a{provided: y>0 && x <1: do : x=0}
edge:P:l28:l29:a{provided: y>0 && x <1: do : x=0}
edge:P:l29:l30:a{provided: y>0 && x <1: do : x=0}
edge:P:l30:l31:a{provided: y>0 && x <1: do : x=0}
edge:P:l31:l32:a{provided: y>0 && x <1: do : x=0}
edge:P:l32:l33:a{provided: y>0 && x <1: do : x=0}
edge:P:l33:l34:a{provided: y>0 && x <1: do : x=0}
edge:P:l34:l35:a{provided: y>0 && x <1: do : x=0}
edge:P:l35:l36:a{provided: y>0 && x <1: do : x=0}
edge:P:l36:l37:a{provided: y>0 && x <1: do : x=0}
edge:P:l37:l38:a{provided: y>0 && x <1: do : x=0}
edge:P:l38:l39:a{provided: y>0 && x <1: do : x=0}
edge:P:l39:l40:a{provided: y>0 && x <1: do : x=0}
edge:P:l40:l41:a{provided: y>0 && x <1: do : x=0}
edge:P:l41:l42:a{provided: y>0 && x <1: do : x=0}
edge:P:l42:l43:a{provided: y>0 && x <1: do : x=0}
edge:P:l43:l44:a{provided: y>0 && x <1: do : x=0}
edge:P:l44:l45:a{provided: y>0 && x <1: do : x=0}
edge:P:l45:l46:a{provided: y>0 && x <1: do : x=0}
edge:P:l46:l47:a{provided: y>0 && x <1: do : x=0}
edge:P:l47:l48:a{provided: y>0 && x <1: do : x=0}
edge:P:l48:l49:a{provided: y>0 && x <1: do : x=0}
edge:P:l49:l50:a{provided: y>0 && x <1: do : x=0}
edge:P:l50:l51:a{provided: y>0 && x <1: do : x=0}
edge:P:l51:l52:a{provided: y>0 && x <1: do : x=0}
edge:P:l52:l53:a{provided: y>0 && x <1: do : x=0}
edge:P:l53:l54:a{provided: y>0 && x <1: do : x=0}
edge:P:l54:l55:a{provided: y>0 && x <1: do : x=0}
edge:P:l55:l56:a{provided: y>0 && x <1: do : x=0}
edge:P:l56:l57:a{provided: y>0 && x <1: do : x=0}
edge:P:l57:l58:a{provided: y>0 && x <1: do : x=0}
edge:P:l58:l59:a{provided: y>0 && x <1: do : x=0}
edge:P:l59:l60:a{provided: y>0 && x <1: do : x=0}
edge:P:l60:l61:a{provided: y>0 && x <1: do : x=0}
edge:P:l61:l62:a{provided: y>0 && x <1: do : x=0}
edge:P:l62:l63:a{provided: y>0 && x <1: do : x=0}
edge:P:l63:l64:a{provided: y>0 && x <1: do : x=0}
edge:P:l64:l65:a{provided: y>0 && x <1: do : x=0}
edge:P:l65:l66:a{provided: y>0 && x <1: do : x=0}
edge:P:l66:l67:a{provided: y>0 && x <1: do : x=0}
edge:P:l67:l68:a{provided: y>0 && x <1: do : x=0}
edge:P:l68:l69:a{provided: y>0 && x <1: do : x=0}
edge:P:l69:l70:a{provided: y>0 && x <1: do : x=0}
edge:P:l70:l71:a{provided: y>0 && x <1: do : x=0}
edge:P:l71:l72:a{provided: y>0 && x <1: do : x=0}
edge:P:l72:l73:a{provided: y>0 && x <1: do : x=0}
edge:P:l73:l74:a{provided: y>0 && x <1: do : x=0}
edge:P:l74:l75:a{provided: y>0 && x <1: do : x=0}
edge:P:l75:l76:a{provided: y>0 && x <1: do : x=0}
edge:P:l76:l77:a{provided: y>0 && x <1: do : x=0}
edge:P:l77:l78:a{provided: y>0 && x <1: do : x=0}
edge:P:l78:l79:a{provided: y>0 && x <1: do : x=0}
edge:P:l79:l80:a{provided: y>0 && x <1: do : x=0}
edge:P:l80:l81:a{provided: y>0 && x <1: do : x=0}
edge:P:l81:l82:a{provided: y>0 && x <1: do : x=0}
edge:P:l82:l83:a{provided: y>0 && x <1: do : x=0}
edge:P:l83:l84:a{provided: y>0 && x <1: do : x=0}
edge:P:l84:l85:a{provided: y>0 && x <1: do : x=0}
edge:P:l85:l86:a{provided: y>0 && x <1: do : x=0}
edge:P:l86:l87:a{provided: y>0 && x <1: do : x=0}
edge:P:l87:l88:a{provided: y>0 && x <1: do : x=0}
edge:P:l88:l89:a{provided: y>0 && x <1: do : x=0}
edge:P:l89:l90:a{provided: y>0 && x <1: do : x=0}
edge:P:l90:l91:a{provided: y>0 && x <1: do : x=0}
edge:P:l91:l92:a{provided: y>0 && x <1: do : x=0}
edge:P:l92:l93:a{provided: y>0 && x <1: do : x=0}
edge:P:l93:l94:a{provided: y>0 && x <1: do : x=0}
edge:P:l94:l95:a{provided: y>0 && x <1: do : x=0}
edge:P:l95:l96:a{provided: y>0 && x <1: do : x=0}
edge:P:l96:l97:a{provided: y>0 && x <1: do : x=0}
edge:P:l97:l98:a{provided: y>0 && x <1: do : x=0}
edge:P:l98:l99:a{provided: y>0 && x <1: do : x=0}

[fredher]

Dear Ocan, Clock bounds computation follows the algorithm presented in "Bouyer, Fleury and Larsen, TACAS 2003 and "Forward analysis of updatable timed automata", Bouyer, FMSD 2004.". A short description of the algorithm is given in file include/tchecker/clockbounds/solver.hh In short, we compute clock bounds by solving a system of constraints with one variable per clock and per location. The solver used in TChecker is based on a DBM representation of the constraints. In this settings, clock bounds are obtained using Floyd-Warshall algorithm. This results in a (n*k)^3 algorithm where n is the number of clocks and k is the number of locations. This grows quite fast. This approach is good for systems with shared clocks and extended resets. However, a faster bound propagation algorithm can be used, at least for subclasses of timed automata (e.g. no shared clocks and resets to constants). I will improve clock bounds computation in the next weeks and let you know once it is done. Best regards, Frédéric

[fredher]

The latest commit should fix the issue, as well as a bug in clock bounds computation in presence of complex resets like x:=1+y. Best regards, Frédéric