cs-au-dk / mona Goto Github PK
View Code? Open in Web Editor NEWMONA - a decision procedure for monadic second-order logic on finite strings and trees
Home Page: http://www.brics.dk/mona/
License: GNU General Public License v2.0
mona's People
Contributors
Stargazers
Watchers
Forkers
codelion pombreda cordarei ya1gaurav muylor ondrik liyong31 whitemech nekdozjam weltoph meitinger tmbrbrmona's Issues
Possible Infinite Loop
unsigned_log_ceiling function may end-up running an infinite loop:
unsigned unsigned_log_ceiling(unsigned i) {
unsigned j, k;
for (j = 0, k = 1; k < i ; j++, k = k << 1);
return(j);
}
If paramter i has a value between 2^32 and 2^33 - 1, k eventually becomes 0 and loop runs for ever. That happens when someone tries to create an automaton with number of states greater than 2^29.
Reduce optimization breaks variable order in import
When import is called such that the order of variables is to be reversed (unavoidable in some cases), e.g. when computing composition of two transducers:
var2 x, y;
ex2 z: import("rel1.dfa", t0 -> x, t1 -> z) & import("rel2.dfa", t0 -> z, t1 -> y)
when using the code optimisation ("-o1", turned on by default), even the technique from MONA manual does not work (note that it is required that the order of variables in the imported DFA and the order of variables assigned in their place need to match):
var2 x, y;
ex2 z, w: import("rel1.dfa", t0 -> x, t1 -> z) & import("rel2.dfa", t0 -> z, t1 -> w) & w = y
because the optimiser reassigns t1 back to t1 -> y in the second import and MONA crashes. As far as I could tell from my example (attached), setting -o0 when calling MONA works, or removing this line works, but the second solution is very ad-hoc I'm not sure whether it really fixes the problem.
Possible Infinite Loop
memory explosion
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
error when `make` front
wsl2 ubuntu20.04 .
flex version 2.5.4
bison++ Version 1.21.9-1
Linux tridu33 5.10.16.3-microsoft-standard-WSL2 #1 SMP Fri Apr 2 22:23:49 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux
when i run ./configure,i just try make command:
g++ -DHAVE_CONFIG_H -I. -I.. -I ../BDD -g -O2 -O3 -DNDEBUG -Wall -Wno-unused-function -Wno-unused-label -Wno-sign-compare -MT mona-parser.o -MD -MP -MF .deps/mona-parser.Tpo -c -o mona-parser.o `test -f 'parser.cpp' || echo './'`parser.cpp
parser.ypp: In function ‘int yyparse()’:
parser.ypp:171:74: error: ‘yylsp’ was not declared in this scope; did you mean ‘yyvsp’?
171 | {$$ = new Assertion_Declaration($2, POS(@1));}
| ^
parser.ypp:36:20: note: in definition of macro ‘POS’
36 | #define POS(p) Pos(p.first_line, p.first_column, file)
the same result happen when I go into the path ./Front and try g++ -DHAVE_CONFIG_H -I. -I.. -I ../BDD -O2 -g -g -ansi -pedantic -Wall -Wno-unused-function -Wno-unused-label -Wno-sign-compare -c -o mona-parser.o test -f 'parser.cpp' || echo './'parser.cpp.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.