Extremely slow clock bounds computation
osankur opened this issue · 2 comments
osankur commented
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 commented
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 commented
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