search

cs-au-dk / MONA

MONA - a decision procedure for monadic second-order logic on finite strings and trees
http://www.brics.dk/mona/
GNU General Public License v2.0
48 stars 13 forks source link

memory explosion #7

Open melbrbry opened 2 years ago

melbrbry commented 2 years ago

I used -s option to debug and it seems that the computation are all fine until it reaches 99% then it stucks there and eats all the memory. I even tried using 128GB memory, but the same bug persists.

input:

#F((at_p2 & X((collect & X(F((at_m2 & X((deliver & X(F((at_p1 & X((collect & X(F((at_m2 & X((deliver & X(F((at_p1 & X((collect & X(F((at_m1 & X((deliver & X(F((at_p3 & X((collect & X(F((at_m3 & X((deliver & X(F((at_p1 & X((collect & X(F((at_m2 & X(deliver))))))))))))))))))))))))))))))))))))))))))))))));
var2 $ where ~ex1 p where true: p notin $ & p+1 in $;
allpos $;
var2 AT_P2, COLLECT, AT_M2, DELIVER, AT_P1, AT_M1, AT_P3, AT_M3;
(ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & ((v_1 in AT_P2) & (ex1 v_2: v_2 in $ & v_2=v_1+1 & ((v_2 in COLLECT) & (ex1 v_3: v_3 in $ & v_3=v_2+1 & (ex1 v_4: v_4 in $ & v_3<=v_4&v_4<=max($) & ((v_4 in AT_M2) & (ex1 v_5: v_5 in $ & v_5=v_4+1 & ((v_5 in DELIVER) & (ex1 v_6: v_6 in $ & v_6=v_5+1 & (ex1 v_7: v_7 in $ & v_6<=v_7&v_7<=max($) & ((v_7 in AT_P1) & (ex1 v_8: v_8 in $ & v_8=v_7+1 & ((v_8 in COLLECT) & (ex1 v_9: v_9 in $ & v_9=v_8+1 & (ex1 v_10: v_10 in $ & v_9<=v_10&v_10<=max($) & ((v_10 in AT_M2) & (ex1 v_11: v_11 in $ & v_11=v_10+1 & ((v_11 in DELIVER) & (ex1 v_12: v_12 in $ & v_12=v_11+1 & (ex1 v_13: v_13 in $ & v_12<=v_13&v_13<=max($) & ((v_13 in AT_P1) & (ex1 v_14: v_14 in $ & v_14=v_13+1 & ((v_14 in COLLECT) & (ex1 v_15: v_15 in $ & v_15=v_14+1 & (ex1 v_16: v_16 in $ & v_15<=v_16&v_16<=max($) & ((v_16 in AT_M1) & (ex1 v_17: v_17 in $ & v_17=v_16+1 & ((v_17 in DELIVER) & (ex1 v_18: v_18 in $ & v_18=v_17+1 & (ex1 v_19: v_19 in $ & v_18<=v_19&v_19<=max($) & ((v_19 in AT_P3) & (ex1 v_20: v_20 in $ & v_20=v_19+1 & ((v_20 in COLLECT) & (ex1 v_21: v_21 in $ & v_21=v_20+1 & (ex1 v_22: v_22 in $ & v_21<=v_22&v_22<=max($) & ((v_22 in AT_M3) & (ex1 v_23: v_23 in $ & v_23=v_22+1 & ((v_23 in DELIVER) & (ex1 v_24: v_24 in $ & v_24=v_23+1 & (ex1 v_25: v_25 in $ & v_24<=v_25&v_25<=max($) & ((v_25 in AT_P1) & (ex1 v_26: v_26 in $ & v_26=v_25+1 & ((v_26 in COLLECT) & (ex1 v_27: v_27 in $ & v_27=v_26+1 & (ex1 v_28: v_28 in $ & v_27<=v_28&v_28<=max($) & ((v_28 in AT_M2) & (ex1 v_29: v_29 in $ & v_29=v_28+1 & (v_29 in DELIVER))) & (all1 v_29: v_29 in $ & v_27<=v_29&v_29<v_28 => true)))))) & (all1 v_26: v_26 in $ & v_24<=v_26&v_26<v_25 => true)))))) & (all1 v_23: v_23 in $ & v_21<=v_23&v_23<v_22 => true)))))) & (all1 v_20: v_20 in $ & v_18<=v_20&v_20<v_19 => true)))))) & (all1 v_17: v_17 in $ & v_15<=v_17&v_17<v_16 => true)))))) & (all1 v_14: v_14 in $ & v_12<=v_14&v_14<v_13 => true)))))) & (all1 v_11: v_11 in $ & v_9<=v_11&v_11<v_10 => true)))))) & (all1 v_8: v_8 in $ & v_6<=v_8&v_8<v_7 => true)))))) & (all1 v_5: v_5 in $ & v_3<=v_5&v_5<v_4 => true)))))) & (all1 v_2: v_2 in $ & 0<=v_2&v_2<v_1 => true));

output log file: log_output_file.txt

amoeller commented 2 years ago

What makes you suspect there is a bug (except for the reported memory usage "0MB memory used")? Note that the each quantifier may cause a worst-case exponential increase in the automaton size (see https://www.brics.dk/mona/mona14.pdf).

melbrbry commented 2 years ago

why the -s option is not showing what is going on when it crashes our of memory? why it is just stuck for ever at 99%? also why I do not see any info about how much memory usages are used?

as per the documentation -s option should be used for detecting what exactly causes the state space explosion.

amoeller commented 2 years ago

It is showing what is going on:

Projecting #49 '/user/brussel/106/vsc10621/.local/lib/python3.9/site-packages/ltlf2dfa/automa.mona' line 5 column 2
  (ex1 v_1: v_1 in $ & 0<=v_1&v_1<=max($) & ((v_1 in AT_P2) & (ex1 v_2: v_2 in
   ^

Feel free to add more logging info if you want to know what it's doing in the projection operation in more detail. But it's probably not going to help you, for the reason I already explained.

The reported memory usage "0MB memory used" looks wrong, but that's probably just the memory usage measurement that is incorrect, which is unrelated to the actual automata operations.

If you send me (amoeller@cs.au.dk) your input formula, I can see if I can reproduce the out-of-memory situation and look into the incorrectly reported memory usage.