From 41be2f07c7810ecb7681211a7de77cd4019aff93 Mon Sep 17 00:00:00 2001
From: Thomas <thomas.vogt1@rwth-aachen.de>
Date: Fri, 14 Feb 2020 16:31:35 +0100
Subject: [PATCH] kiss parser
---
asmlbenchmarks | 22 ++++++++++
asmlbenchmarks.csv | 22 ++++++++++
asmlbenchmarks.ods | Bin 0 -> 22700 bytes
learnlib/GraphvizParser.java | 28 +++++++++----
learnlib/Kiss2Parser.java | 78 +++++++++++++++++++++++++++++++++++
nfabenchmarks_pgf2.csv | 8 ++++
6 files changed, 150 insertions(+), 8 deletions(-)
create mode 100644 asmlbenchmarks
create mode 100644 asmlbenchmarks.csv
create mode 100644 asmlbenchmarks.ods
create mode 100644 learnlib/Kiss2Parser.java
create mode 100644 nfabenchmarks_pgf2.csv
diff --git a/asmlbenchmarks b/asmlbenchmarks
new file mode 100644
index 0000000..6982e39
--- /dev/null
+++ b/asmlbenchmarks
@@ -0,0 +1,22 @@
+file,origstates,forward states,forward rounds,mqueries,reverse states,reverse rounds,mqueries
+../../asml/m106.dot,79,79,25,2980800,96,38,2494380
+../../asml/m135.dot,57,57,19,3115636,66,26,1754456
+../../asml/m158.dot,28,28,12,338013,35,16,281952
+../../asml/m159.dot,30,30,11,369680,37,17,311740
+../../asml/m164.dot,43,43,8,430544,48,22,575498
+../../asml/m172.dot,113,113,36,7166880,119,51,5936328
+../../asml/m183.dot,9,9,5,4368,11,7,5700
+../../asml/m185.dot,190,190,39,15340536,231,50,15922095
+../../asml/m196.dot,81,81,33,2573870,89,58,2970903
+../../asml/m199.dot,27,27,15,223008,36,18,264762
+../../asml/m201.dot,128,128,46,13830919,145,68,16272915
+../../asml/m217.dot,14,14,10,182643,22,12,207944
+../../asml/m22.dot,93,93,28,4605436,117,46,5020006
+../../asml/m34.dot,115,115,35,6555594,123,47,8157072
+../../asml/m41.dot,25,25,9,97550,34,13,147465
+../../asml/m45.dot,184,184,52,10515860,219,70,15981504
+../../asml/m49.dot,142,142,36,8028494,151,65,12654375
+../../asml/m54.dot,27,27,13,83237,29,21,131670
+../../asml/m76.dot,210,210,66,14901636,245,80,20917533
+../../asml/m95.dot,33,33,11,390710,39,18,306348
+
diff --git a/asmlbenchmarks.csv b/asmlbenchmarks.csv
new file mode 100644
index 0000000..6982e39
--- /dev/null
+++ b/asmlbenchmarks.csv
@@ -0,0 +1,22 @@
+file,origstates,forward states,forward rounds,mqueries,reverse states,reverse rounds,mqueries
+../../asml/m106.dot,79,79,25,2980800,96,38,2494380
+../../asml/m135.dot,57,57,19,3115636,66,26,1754456
+../../asml/m158.dot,28,28,12,338013,35,16,281952
+../../asml/m159.dot,30,30,11,369680,37,17,311740
+../../asml/m164.dot,43,43,8,430544,48,22,575498
+../../asml/m172.dot,113,113,36,7166880,119,51,5936328
+../../asml/m183.dot,9,9,5,4368,11,7,5700
+../../asml/m185.dot,190,190,39,15340536,231,50,15922095
+../../asml/m196.dot,81,81,33,2573870,89,58,2970903
+../../asml/m199.dot,27,27,15,223008,36,18,264762
+../../asml/m201.dot,128,128,46,13830919,145,68,16272915
+../../asml/m217.dot,14,14,10,182643,22,12,207944
+../../asml/m22.dot,93,93,28,4605436,117,46,5020006
+../../asml/m34.dot,115,115,35,6555594,123,47,8157072
+../../asml/m41.dot,25,25,9,97550,34,13,147465
+../../asml/m45.dot,184,184,52,10515860,219,70,15981504
+../../asml/m49.dot,142,142,36,8028494,151,65,12654375
+../../asml/m54.dot,27,27,13,83237,29,21,131670
+../../asml/m76.dot,210,210,66,14901636,245,80,20917533
+../../asml/m95.dot,33,33,11,390710,39,18,306348
+
diff --git a/asmlbenchmarks.ods b/asmlbenchmarks.ods
new file mode 100644
index 0000000000000000000000000000000000000000..d6b58924dcd4c8ba9077117eb2a8e67fefab3d49
GIT binary patch
literal 22700
zcmWIWW@Zs#VBlb2=neA=Xw9+g(qmv?0AUUW28P_s+|-iFg4D!<f}G6c#FEVXJpHn~
z6utb!;>=>b{DRcHl>Fq<+|;}hz2btR)WnqHjMUT;h?yK59AGmUkO0`s)RIKKirk#u
zN#6ap6+~LU{}mN8j%Gf_fAmD+61`osR!yDdb=Q^e&c_Qv9XxW&|L?0a4^F+P+W!7d
zb&b#065H7?c%#<Oy}OttSfp{PU*_#M7r!4~UeP}9Nc*Y1donm<EN{*|*!F{GVISM-
zuX{458dZOhI@BtB>AUT_;5WD047`Fb352#=)m^?|zu@S@Ikzjy8Lj!_Z6#-(m$sez
zZAG?j`PS?6ZvWz$$9~fNvsCB(OEteHMDCQzt-pJE`jk}9Ww%8`iyrI6W~+I5GO-=w
zou^`<sBLZbVgEw6vc4@xc5BX2+_=p;X;IK5{;7=#Q!dWfWO0(u^HA}z$j0tPOLUg+
z-lL=)=6l%jrNN&~5v94ZZ6_bSR`j-i{&RcRo&ELsllL!W)IU}K!gbzFHXWX{>s{%!
zSr1Q7nJHp%R5ERbon7|r*na!6qZ>~wl73Q=dDnkJ<B~5Qlb82)-Q4u-{gKMU-*(kV
zIQ?3XYVvZSon*(-*EteW&YLw3&InB|*}meP$+}x5E-tS3wtBzYoAQx8z?+>z^%Sd2
z6C(oyJ2L|VB;H_Y0V&!TBp4VNob&V2GSf?oz^S0vNWUaMKPM@%NFTQ@87#UAit^Ko
zQj3f6>y*Nxv$!O&q?CX@Y&Iq)C#UA57A2PC<8v!EAExExCzhm=sw+1&uatD(fkLw&
zF)uX-Pk72>36;#;#Prl+eW%Ql+{A)nJesiuX+eHLX#vQ+P<`04EDxv{NX*MjOD!(Z
zD@sW_JNay0vw=X%dz;qOb2l9HSy_uTPVLN^f55aYf>r<1ETMb*`X+}3E?M<z{*}k;
z+>Gz{ZJGTxQRYPVrWFT6Op-NKPkCf)eW`7=TW{ym+g7)3Y}1yXCHpa}dFgzuUFCUN
zmhsbCb<KHl&Tn3%Q8DYYjsG5{gI6sIJ$R07>Eqy(>vhWf`lLq6^4ufNwD7=^*9#_8
zepj&VzH7B|!6vT6Z9#k6w<%0)bm-;uIn`3qEVIkc`>64>&w-W)7ruRTJYnzU=0!FM
zAGG_<-?-Pov+QZygS{Kx#WdfqnVM1cF1f1o^3jj?m8T@kF?#3!YPWUe|L6bo&i|Ku
zw0=vOOOC_2#p%B$Jm2z3KGc0ZDCcbXo^gqlk%6HZo^!ATA2$O7Lvnsz38;vy$jx~g
z8{L1~OswvHykSA((RYV-O}KJ(w&%qyyq_i{iRX$(EYM);bGd!%#3b#Lk7xe-_0;u}
z$G)#81l=zm;Y>SrW#`8Ue=0madaU19cVmh9_ca=mZFbL9ygcvj2AxxnRif{n`}g^C
zwDOGFzrXa?e|l=vc|+;k;=66BQw5(!9<9G$@NP{^4tLn6{4JB5%3Qad$ecN)yC*MV
z=ZZzH`%)th@3wdr>9KcJP3V!rD(mR*t7VCizyIF5BW$c6Cblg%Y3-UBVOMte-}tw>
z?Qvpku3ymt10LPVt*W|{jTcS)dSCwDf04B}+oU|h!c4kv2#5bU9;5rwNZ;(KWL3_}
z)4YXq^3Qoa6Jgu^TrX?o=@lN^M6Vp|+VwhWq0}kejNN;rqt>4PVX>j^f%wyY`Fq<<
zwO`1s^1krt-?dP2ah0~slXsks-pIaTGE46C?Q7(M*}iR1cxTxeDsoCEWA~oQdE5Vq
zKFK;_diUVQE8p9!&d%40Tyv{%=b7@zHEmNaot4|R#^Z?UEWKBbcP3s~{p&AR%*WrN
z?hR+BW$$`jtq|{&`o#NO`}`j*nFVo?6XUM8eX^Ufa^sovGxqyL-1@S68?WCkqw~GK
zCnqjSa@`kOvSarnxl1a)E97P#x%%!#O+%*GfeFV?J3nP-HtUNzdOLQa*Ve+6jZ-)s
zm$v$(m~Oc^OYDK7a_8<@T#cUT)$6iFb7qT&T3fx8t!eRmv~JxB9naEJi|zksbY{0n
zT*%$K>F%>W(FB=?#-}e%c*eVTzlGj+*F&=xI?KhX^k+zYjVY|W(>_flYxVh^>m`0P
z<zAe8;ds=p{TZyAbRCU%udGg0k2$dUx^K>cXR|M5aZj^xGni(Q<aTD!mYTm_mfLmr
z1>SGnyM6O_&V0?t#@X{TjxD$8Gvs}#<|&__UcdDAo<GkS=W5Nl`^AO3D*33<JBE7_
zPwg~M%N;dasbn|v?q#Kk=eFw2{uVn?edCp~&$7FhOU4!++srm^N!yH{5n(yTlji1U
z&boK;h4PV8ZDl6XYm48;Prn>H^>cwzCy(axw-TSy*SiJwMWt^2S!7Z0#jkvJ&b5Lv
z?q1#FE@2^@+WFIdK3bRXWpUwg3!9=wr&8sOYWLMQcI0$;=BVHD_-*|xW)rXd^xP9X
zcM4|YKG~Ubc$xKu+;g92K1(z@WA^>$tSjXo4Q}sA&k53(NSpn?C-)VP4A;TWH{0$y
z)@h$R7(MYlKhI;;*wt5519zmI%sR`=bh{*_eOJzhbt!K9)=uK}?bRy}eIs$_UDv#A
zyEX58Fz6CJHf`OEK!4vH&+^RDfR%o&Aq&LSpPDW0-)g(nL@?pw)rA{RChKYH_Pok-
z_`JE;n8W+>vs2T=lKh?Pc4llyuzDj?^DIVG>6g%4_2&nlg`Zw}*1kYG{OH8q)lGTV
zJ+G`<zrVb+yQ7C&`%{06%e3@6@tZPcF3DW);BsV7)0K$luAi#)n4FrIozxP(cQWP8
zt>wGLr535L@)bIssjT}vPoQ36%biUf<+3d6U+nLHb<);9^=^gl)ut~ozSdW>4lkJY
zdx5WuFW;()l*OfH5-auZJpK4MIA{0MzRuI8$yZ;8uUg;bP&NIO#}$o8)m<5vd*`R<
z3E$HXsycq@Q`xp9nJ4eA$T;GmbEC^!gGX+)_!<$#ubQiBCmj>iee@}F#;Wd5>Aovu
zd`|mT9p99(cj3|Fn*=Yty`J>K?9bC#d9JNf>$&S<cm68hx2Z=mzUS8FWz%grC(PaY
zR)4Rd^6csDv(Ji%&+0pp6?sE}x5%e|!m=sa2aoW~U7-1(_RzEX>uyiW|39wvS$X=C
zR-~QOo!h&0<6joYL`$)r4O?TgX8TXxIGL#nW;ZX&zo>X|`*9QZrhT?zU%q)<xSc#p
z*)hMLb+4t+muEAcd0db_b60P>kl5=c-Td@rU-h4E+qS3b&ZlRZlh1~&Q%Q~7DfT+*
z*!AOu!7hulj>}eCpWgi4viG*)PSNJ&m*q+yfACB>>X-FzVxdU?tJ=1SJ(;-^WWPEs
zcRhb4Q?Sf>uGmh~`|98BEY|yQHc*`5>$~^;EVcDM#VRj;Cp*6HW7%uH%u?u!U;X=I
z`YX%pR~feNz5PnLg#G<%fv+rEP9H6jbzk|y^{DppLsHy2!r2o%O-_`UoG39p@x|oC
zm;WlI{8BTs;<u^kR?2KituZ+w6TbfHDRE=<kS^A1jioVhyL&w^%NoBDj25+Nn0?pe
z_G0yQg^oh{ai0UGd=y-@&&2tw=bs;3m3Q`OX}??eDe~&4r;q0ypKC6>Y8v<I=b?Ll
z<{s~QGV^t`!N%q1mKBsP{^kGpm3@oAYX`pLZ7&ZbH8Uk0t28Z=^`E)br#R~C`a9<i
zT~5=wb?wxL$+!P5DH30D=j!4+ig65=^f|uHXb?ET(DG%)cgI_`zPayjo2~h2`OtK+
z^PLa(mQFc-;q=kB_v;>NzlvWQ|AXmoIP>4X@*W!Pv${5R?v|f$Q{sHJ&-@tHNM`42
z2@Nj|qV=V|HysdCuJ_vD!k4qhYSsfLvxEx=9x{c=C!AL_5LQ_!XMEtX|77umR}<B~
z-uULsevMc3rN#wMm6AyhFTDJvR#fod*H?dqN9U`3k{#41UhrgdP}i~8AtSj*;YG=X
zDJMD;7s_1|dF?Cpv~Az(LldHdUKutWFlc@;YgfbPwq=&gmirzb+_gYSmeo|YbJn?n
zD=KnpHtsQ;aB<>^7d#Hf4BaksJGqIpO?Fbwk!&+vdsv_#BEu=Ir!)8PvMAS8oN`}#
zEGja1c~+a6Ha-6#XRv14lEnuWYd^fWmr1VEbC-O?<%yO3nLIB_R7-Zn>y_*}H@#=h
z<zps{2U(smc&_BMOpukz=2~l*<Jf7MyFjVQMt+B;vZwn&U;jtT%w^1LFK_(2{J+70
z@6T(O85UfgyyIo<&fham@T#%;B^+4#dRzNE-7Sx=O<rF8FwixDSuu8ER+mfSM~jOh
z{mKyvJtnM&EF2bc%e<LXBI5E@b<wZzJCc_+uPv1_t?iukkKu~UW48O<PG>#EU$K~7
z7LMH>|K*O(zmO|mob(y2+$Lo?`9_3a7iCkPQMJU=*0F;<-GJZYQec4bgcXu8jkB(=
zxxcaPYqf%)>5n2o(-L*okc=%~T^X}7ejkwj+Z7_b<bc>Wm&=Fh9`ObyRUc`bxxmAn
z@k#(wmW50}V8WsYFXam=MbA|GBr{}bFq+CRtl04M*wd@WxS2wp`0i5XvYEH|b;daf
zceQn4?*wkM&g%(WGV2V3oYvJ+?etrh1J}K`Qar=lRU-1hWt)rNzif*VrOSuwGO8E8
z|H)V2FS4)_6yzeuR$K8{#F`%Z`EokTyp&4?S6W%WuUluTqVvd!S$Um5ue)H8?TfpG
zuB(sR${7S**lNfb++Qjy@F3ykjstrmU9I^xDYdS7!Ie_#YtJD&zoM~uBCl<l(R;(*
zrZpal+P{k4Usk?7TPU)2hIMUhd1vXnOYyyHEO_29%wP__{HoBOqj_q8@D{-bR?*=H
z-n8&BzDu~i<*~wQFL$TwPm~oeyE;nzIO4dEzxT(*J;zPBHmzz=F;P*@oU``R^p>>`
zm)wv#P-e*N>z<%?@9@!e{!9-9=gbPbe2qP)i@PNC64UiNyBtiuyuHA7??m91#|<mI
ze4N5l)LPRXRIhX1AbZL_q4>d`^Cny!tFEYgVSTQaXp_lhv*v!=E`^+1ha>vZKlAZ&
zGiFD{Zhzb`v2oq*7kpPZXDQq{wk`K?&Wg<A2Lq-qYgu<9_|Q7Z8}lA3@h9@VJm7F;
z?)MpP2Lq-aX=zI_OiU1an>wN1QKRdRXQGJX`NP@PmMe|3-@QuR*KecGuueZaD)tB0
zodmgEhk4j6625I;HnmGysGmXo_N+3Qn$SwW7hNvu*Hy|+h`-TOx>4Ssx#u0ox%*c6
zsGF!<eQCUVv%lKjjr|KUXYKlAqHZ_s-OfM4hu9o^S97`=7EC)lE6tK!Ox1c;(-VfB
z``#W_+B>UEMkF-S|3%jp_47Qj=Z~IHS5z|l(9vQ3-nh4Ek=A=oUeB6ecfx*sThg!S
zc;Kh}%jjJHUB_Hh9voye5m?h{I`fgk{NoF=y&6kdbI<?#yrJLu#g;hXe&(fGcR6Dx
zzHjO1WM<hjzw1PdP(RaLt)HB{C+mK_d1qodd6~W9i-$WFK7XhdcfUD3Nt&I{fMso_
zsUmxUVsFXXC5`?;Qolr0f2io?9sJ=Su&VR8qu<m|E$dEHe)5@Ua^~X&?%XE~^D7>o
z{q3_@VWn4<lk=u|cAGB;oLh3-Cy?Q=fZy^=WuCUj&c&+_e%&7XgiY>C<g%`a%WKUO
zRC-ET4<4Azy^Bv*!Td>fiS!Nm>_>$YLY`VJ%$_vY>2lunrx$c|Mb1@&3_exn<a}xF
zv72tyjuBl=nFmc+9(nwj`OI_Ik&UqlDR%_2nSz;WB!n-PHnab*sjN-t+9>OEey8@M
zzyl(yzo^%^{+evzb<47Vzjn^GJ;zPhW+YAh*V4Yk-qN6W?rFAt3I<=*Z9TghGoMF<
zpZj@4)9%E>)jApLf}PiJdN<Bq9C7`b#)kt<>o#-ANKJh2G@mC(xW9R+)<e$t$seA~
zjC;;}r}oP;+hu_pLR4)YDsuYoV!E8?8O+$Yu<-lZZEsKCN;*{^{P9)v≀cAKe>%
ztM11K-)ZUnvuncZet7Pw|9-eU->zoE?C(cHw?u68`Y37A*XnlQcf$RL-(ou_Rwx%8
zGAuotai;6`FV;Q1nW=FhclY=1KE5neXxgzhrnH~8E-v47Wnb=n<~x<DQzxa*UG;rt
z(z~V4QjhMvE@0mJ%Jt~k?H2uIkFHK>TOt1c@2~%$PT=8Jz9wgQ85kaQ!-h|=bpk<s
z=;G9plFYpHV$jgn+o<T`TNWa9_v0r%ELA`1Fp1a4>9|0iuE2&~#k$G4f*~m<l}}3i
z_^K`aLgmW4pyu6geJUAmTiv&``*qIu@ZsZI+t-IpD0DfQyzq;oW{l&b0P%^}j~_ac
z5r1FY?%MyV1)nX863#C5d*G<F&Qiol?_qe*oDZ{{Ps(^UHcXUamH8;eDEGwl;guEq
zCmq*(D=XCv+qQf2u?`)1Zf?atQ5z-N9=31z)VS$-(#oi{Vvm=%FSYje3*EZ?cdwS$
z%W&6;2l8CktXZRBe)MkX!z}%u$4s9({e94W`1N)9Z|^t#-sQ$rH8FqPx9!T8<+y`V
zb6XRBT+MD(+4<c_?a_&20jUBKSM+7%x_b5Hm6W(jpDz5NdxD?w`@@(g%{H#<B2*mj
zhrD}#I{k3DVpXilthm5a+s&6himyJf-|a|i_6xb!O^KiMjv7sh&nfOYYVc;Kds@*!
z6;`gV9Rf?`H<>WmZo15HN%?>3i)z6GwmGK-;wu_-{S%Xn6Xt9ZeClz+VTNku-dVZs
z_m%gnd{R{w-#ulat}0W)-QylSE4cf=CpzAgjA{2#P}l#W{F+~GSIU}wTkY9vt_o(b
zCYSI|xGwTN<qQjZ_2p03?^bSziYhw!qMP|$>gOMfTOC^$#0eExE|%BvvUNTbGv$)t
z3eJLp9;xW4Q&P{AKX5J9`5pUZch7@gO>MGmeZo6@HQO3QUNx~AB$u4{;w@RiyF={!
zro%ImrM^AXE-=g7^^D=ONGhlKeX*5Wju)C*nof9ZH96?SJ@F}<h36gCIA)fxQrG3>
zw|D>eH=b85Te3hgdgarOgDXT&I_wF)5;5W8jk>y@8eJdSL!PkC^?%{M!naG)dx`hY
zbwPUf)6U#}zs;0=c?sk6Y3y<rGj6mVm^wL7&+7|oi&NShnG4l_ECq^Ywfs7^S@W5d
zjougWKq2FO+P67mwh9?}Z}XVq5d5;lZNk?behv8nyakN?o~4|u)(JoTc7N11=aqUg
zDQ2azn`fX=+V12ZM=T%5RM>8a-Qr|(^$&NWy7c_1R@N1zy*u_zWStY(wC$zN-@U)*
z{+%;_PlI#eufTKf+zvP#Stf6Jd7__K!rJ4tli8l1%spX$Gv>~x91ZU7=gB*!*@}E}
zjs6yFx#U8`#8ZL_KUcr>7Jt5a+41?`*xP<FZHO@{na>nH`ROE~Ij!&1Enh_@`CF9i
zf4$Ur%8CfLHy)qDY8I6V3$Q;r{r>2Y^2UZ-wb>;al{)p$H{PGGsBBp4&RFQeAjD^<
z_i*E~CBg+MWxYw09OYEscb}L0c|A>b&4QiQO!aEMK9zD_MQ=Kj&pDY*5!Za2y}iD+
z`g8v$lc_W3D9$Ks=v{2E{>5)k+k5YCHU6Dx{C|F;!F9{G>06i8x=h=BXmVXw{7+W(
z=J`fF&#mfKG%oOMn5!_~YybH_MThwN`tRl*czD;BS@3{as}=w5dhw}87v%d)dARMO
zk@?cKroW#=Z*KghU3W~i*yiRh+r=xVwE6q3*ed&Q%30nSvu-b58XPLSV(H<~72mFG
zGo849+P8?%()C?i{Gux_UM-z$vgFU&q_b6_dqukz8m{Asy0yk$I_db~8=QYbzvK$%
zJ}moi>R*u5?Wz7<kGIx_f8Bp$s@s$GuM%|Xr(ge*y6oY_D^WM@D&|!!ZGF6R-`h-X
zhcjz$YkJNpEWN;U_}}DH>{&X>A5Gtsm|7WCb!|z{E<dx$ly~)~%8b%AOHDWbnf~d?
z0_C{(RX@5@H4=r*k40tgnDj02MpsTw?X_KL8islErf=82J$uDuzu6JbF0|i!a_+^9
zuG@y@S={V?*F)5V&ewjDUbeD#NqxyyQyIy$#fjTi>t4>`F)21QSGzjRY+pG4j$>PP
zZQ-d(pQ8I-+^+Z5@q-*cCb;e`O>&4ya{2JLf-TYCp+V-=%p8|q*9SLQ7VvC#e{~`L
z&og=1qg(#(y7HeDRGgPo7hIUi%D|wjjITK7Vqjn>E~(5(1sCRbqoRu;LwXAn)2!Z}
z30k6|zH!Soo43nuzV&(BuJ+chN<nDJg$5RO2HoBJ>-h6TG~;|uZ=Aexj;GTDYxd_g
z&zTyo9laXsm%e=l_n|KDd_(@dl6pzgCMfOxQuqJMJ^SzL%>M64$n;9u;};S0bjO5!
z6TXXdOLB-O#TMx#2zaht{OIT`MaLt%94y7MCD%uGa;xupcWTYoO=&idJ)QLT&Ykkq
zisRewzcu^k7|&x3l+bI|@tEN9Pxs*OaKA@+>Yw8}k7jM<`m&~3O-DXpF9*ZJ$I%9!
z7F#+jHJ^sG^Xz)*b*jQHG%9iSCd)~?8RwsC<~LaR|JR4?x03F^S7vMKv~1rQb7=a>
zl8>pErcC{jXXMFsd&<>JlbMOEc@tYyXKAh3;2U`?;_UjS*(~KR3&dumw=aA1K;`@^
zBag^X6}8s0w|=ZUGG~RR%k^z(Qc_Xt?x#(b-GBDajHjw=w&WTgxU|wLf~)AFqu)%k
z*f8r$UT;@!DsTFwDQ#e{I%C(K)yWsURg>%VYJxn@MDEP<Fu!^?FsMfE9ZS|WzaKk}
zO%+`(HT4MNvWT@BO-E}4Epqla*A%s77hKj@7j+_G(Oy0aJ;~{%h6~?*X}a*>S=2@W
z@0;!imfvSGeZKnF>c3j6YPx?u+0=gQ_DYA2({)>VzRhtsA@!j`L{3?1`w9vD%b^P#
zxBgbBb(*WSvDDjnx9Ot4D@3~u0wnU&E^psB)9v1|w{tX`V~t%6zX{6(Z`^4RbM3J4
z=QU?`f2mUykjQ=iMp-Mtxry(=0?UQpr{61Ik@6_s-NN|A*{D^b_s$nE{$u){<lmB^
z=%ti=BP&l(eb(uOJ6p=<OmtaqR^6T-*k~jmW3oZq_UM^v#lnBBZ)*BA?k@WASwvg*
zTlY-~o}>5sW;ajyta?y$)e74<%d^+Q=Dw=y(flg2$3-SpW~%l6mTet7RSMLMgB#d%
z*L)FHQqc<8++I^7`<(qzi17=qENAvh2C3OyU2B{q&!|Q49|?$_)Li?%?pt5zj|-sz
zh9W$@rN3mpte-o3W7pjy``7P&b#<N7$GZh#+orF0XkE0&!}jaxt$k7c7R!!!us0tm
zZFp1MoqEDi(en42Hw$@wy<h$G=IrY)&dgqE#<W{%>DM#2Go~I}`K*$ERZZ9|<FbP_
zUvpfK@Tum!cXs2{sVz{Nqpx_OcJlW;qZyN&wHyOfXKGCJQkayGwxDC0^%D!7)k@Q*
zo)gX$ox&EFbM4P$rr*(hf^W_~u<TqqJ8(Di9GAayR2S@Pk=UB#)5Ws7*CW<qi%@F&
zz8On8xMDWHDT<X*y8irX#l3K*-vv5hF)xqia;U8LnP-2YZlU@T;aP0ymRfGrZhNOG
z)URCB>t(s~gT}NCw|~ty)Hm@x_G6vpwk0{=57#fUUzI7{F<ItSZQj2JzRU|{iWnYW
zyByVEx>heX`LDl=)1<^H=l?Z4@F`h+&G1D;uSD6}wl7xSuRKfk%l>xZT9)0i$oTeq
zf*EP^i-KNEE@ms@JlP;`5U77;@nuoZ^2YLGa_?6>HQlx}A>zk=iIw48=7AN(!gKFC
zZ2UMoqxA8VgKD8cCGWQ%*!*7fP5VUF^wN#j->dxDw$a&i{p;gjZUof#z1FkZT$+CD
zjP2HjXsbo-4{g<M@|~L<?Kau%iJZcwgGZC*G#vHZ$6r`$B;Nhmy&&<pf1<Kfy7Di#
z8y)i|_WCEBoh($hgl+xIBkC`&xtW?pYZo4wWpy<*=I)kPkG;9(TiCgXrmk_gaz7}(
z=%{a_b+OR0*Op7CesqZqI{Y(w#fg~-B79Zr&pCfJu9=d{Qn=E7u0q>+i6h^8PChz4
z!S>Dcr3qc}EO|Q%G-|6>-fNb9rhCfRYFQRv`FY1=#_Sg@UoM*^wO^DpX1F=oWp7%j
z`yIw369Sh9{RmWw?0mlJ!+(QmbC%qmRqEAyeB-*0noA|x^6!25a{0N=(d-z{I**Cd
zm5!S2(_FG9OyBR6|BIuWT`n3<oM7?pZt48V6aFjKCjL@dQWM<w_l)IZ{riGj<_9Ou
zeRY1aM&+HGzmHq6`R_kB_0i3{Qab}B4s?ohdEe69nJ}|rVN69%rA&tOj;e@Te!DAe
z8n?O6$=|P)dphveG=1ObMfS1oO^c_${T4X)cae(co86r0A#JrE+Cn!y{oZaAUtzo8
z-RUFWx_wX8?zCkoW;eg|__}VHPU~#uKbOlw_U^xVGvJ`9$KJ!&4|k*+I2W!ucDwn`
zqT7q3)t3HZbBXw`q#&{F#H>%B!o0%1&A4Hv{^Cf2)0;*61K-RFf1FXb%_^o>y4t@}
z=(Fv-0y({Nb3@Lz$*!6|Yc5;UlLH~@{#Ntqes_N9{q(gUjJ<j9DZeKkSF~R7rLj+4
zwy}K2S*sVBg~$G!ZT)x6FY~{sbq{Y<acOC(pbY=5iJv-J7N1ycux&fvckj6i=9+(f
zC2u&fB5nSZyU*5sO?xPo(^HyLuq$d!|1E)%j+&0!_uq(Hx~=H7x-v_>&-m+U<J1eu
zH_ez2KCAw0@2QgOboMj9tW%Wswzd*o*~p0sFKe#e-=Cd#{d$4LD#w4ii>6jp%egI-
zcl-C~%<Yx{-&g(;QQ9H}pU=-Uwy2NT%4B)9`{=JXHG6rUpMLT7RZXGTE7fbi{NI+u
z%WeDnyX)jjCovP&FYlYoR)+>3=&=npV*mSB`NjWb&!2%iZVP)d)Hbm*FlcJwtLcRq
z7#RGMvQm>v6b$tdRsP&C-~L+$0(-xQFIc0swf%ug&T3VrZ$Vpa!*3fKZ4+KoYBMpH
z<M(^(bK)n>F08oos4_oo-t)sb^YmMz=Cp1U`eN2GJ#d4-EXL_p_u2Nx?`!uz`1##o
zwoN`p6N?g-J7tJReP7lRs}Om6itNflh7G)Z=cZ~Z25{Xqn3hm9$)(UGE8v1r(czu1
z9)^bMt`6ny4O3B{V<k0j=?XckV^3dndAjY1Tko0sc7aTn^t$Axj(|CVjc+fuh24IT
zQo?n`Yj#!?$84)<Rf2Qxed#*d?fE+URbN<*UG35K7<Iioz3a*Dg^}ww+DL|KKk4C6
zwK+MdLUJ-+^>&ks%9;DDw=`u(slE4}chECAa)a+Jo1;rb+^U2_GjGc?^B+!mYdL?l
z@IuArMMpf?Rona&X1``OdZHRW&p+30yO>eO?1M4yj;=CjmVSBtul@C4Ub(vq=5N1Q
z{^FqXHqE<p*?u_nXgsu<(<k@r_^N}-bFZztbLG$8KT7w+e)+wN4xZoDY_OS~<NBfa
zM;msp-u*UK@@0$Uft#@wi@SQ)J^J@!jVJFb?xQ_A>DPBU_OIh#{Qvl$$|$Q(25~`K
zeqFEoHlyyQ*2?&N{pkF+%bmHd>K?fF`birD2e-6W@74w**$uOOqMtp`^lFOz{?6q5
z*}TV-j~s6<>hu%;I-P$jZ{3#k-zv9`J0?H8G_7l2Yx0pr#@m%!lUPjuN}iMD+raeZ
zWc!MLTh-RY=AU?VzvFRfruJRwG&xs!_9dCzS9kW`tF&);SjTt4FKVXys~d$YJ}$RE
z@cejo%^xexP0c!0)vGUg$*;GaeWkrm=4xG_+nS8?JUezhu9+7bbxpEDRB?IPlso2s
z#O^HL=0ERSde*m-RrR~2cxyg#HqO5veuU$hm5_z><GsB0&Z;Hv`es}<^7<9BS5s1X
zvh<177oJH>omgJ$w(S4=H~$zwEnKHHcdEBDF)-+J;!F1;$mt$w`uc5*cmHh*p?&Aq
z8<^Z!EH~xPq=(-UgckTuwmrjqLt8g+liC!G2}QT>#qW0woRk?|=ItqbH_}JyMN7)W
zqwDvrN}6c4>EF{Cmrrs(R7yTNxmD);tO-g<g<(tluf^Bf-S&Px{j7iXG?hq~FvIR|
zmYQ1DNv^E*{t0D@VHf#6cNu<5dAn*=%uYRR&xOk@dX}$yuXuiK>zXvTQ;%nqJ!(IE
z(2}Khh4_w@(vP`r>q}bxxpU6q-Kst1Y+Q#gtaY~zoOm}<YUlr-pKi-v?0a(K99Q5&
zC8g()A75{_df4(Y=FY_Lv8H#pj_d5-ZRBy|39HXd&+d-&)UPRTD>o)Zq$Gttn9~s|
zx^_uqG*{TJFRRr2zIt4BPWO(i&FfozS5{j8uD(IU|6iY?+j|}#4u}mB+v623{#ilJ
z&bH(0PEkufvq@8~KJR+vax#J2`ysdTL@xfhI;mfG@;4uuy=&E7ui!Galb7{=32oC?
za8O8+zWXFXXx>RhpK#w5S=uoU^`7j^^`467J`0)T>gyhuv@m-E%d?-)D~qxZKfmUn
z7gPP>&f*1Shu-DbpXA8>yYBIV>r;Ae?riW06g+oos#$dWJCDteUjIF#;{Nr94c}!Q
zVdn11*-yh6rQPQ~DmtIJ)~qkasWZl7#|g)EOVeL2WLwi(>KpTH$?kd9#g>{kE%%34
zSlb-RN{kIxaS8Yu`Q`lmSj)824ets>f7f{bcwob%e%jZA`C@x}VdVqK3ky2k`Hw35
zEancj>HB?QZL8G}gWu9j@qW><YYJv&e|)%AIqFoz<YU@f7aiDcmdo1kU9>q^sr${X
zj-<_D&+;Pz_6nya>^!di`u@C9Rg=u9%CIZ%<{sK(;k}uQFC=B>?5(#qKTBIHwl`GZ
z?S!i(Di-Hoc$S@vT0D1BQOvu9<ElplABMUeaZzerYVn(kTV##G)+pb@%BBC3OG~}O
zmnC^dozt6nV%4oxqW7<Rx#tuzN$z~vc*afg$Di}J9sWglS)J6#P2Jt+H|5OJ^O4JW
zlwuPPDeQH~Rp0c#$?eJ1(Du!5w<+!^D9jH?i}va}`+=jG?S9IIH61VP)V}F;CkNdS
zTqq)=aWI78&u_Eq?IIz2cRykYH#>Ry)s=M~oOOz2U8lp^(qFFIR5&q6==KkfBQwt~
z>{$M{WA?dSzt;ZG%r^XTL84I2tIOZ)Xta~QV&JqSkNDj--RsUA?&K+AI(Xc3iO-du
z>!QMQVvgKva@<$;ch$TVKRCCw2Xn-%c=1N%@uFQ(QS+*{wK+@8ep^|RnpbnC#cjfO
z1EqJn|FeI2dDEWf|9oQ``Px@DE#@I_AFY*rZK~uh7qp$-f6|f0_a_B+9GYmMYBs&q
z=kF1N-`Cxjl>K~|Q<E4Ve}1pQpNTwD`?fkB)x2+%6~25^@t*hFw}{Pe*O}(8IInrp
zp6wsJg!un`*<Ee@Y4L{UJ@2&_ur7}LQ}*=bgWUf0zuR**N_W1p-)>#>{$A^>M%`}z
z*v0oQr>)(y`Csh&MTG_;R+l4RCs`|Ld%u`t^*KSS`t|kZt9_H7oGhBNZS9`8lu7Td
zy;tsP&CuC!E9u@><6Y;ut&gWhRx8Z<A-rDpO0r+v;#;{vJ0^>Mbji<1x7c!}Zt3c?
zb2e}bCM3K&^JiD2^qQGm*F$1foPNS5@GblM(uG$YJSDGO5196aiz)ooQHN{K&DyPG
z9x3%%PW-X)#LH<S7xj++SzS=)x_b3If4f;RrM3G6f7NJzsZsv&X0cf3Df7}<8_OeB
zNb#0!PQAL$c<OVO(*ed)pZ{2Re_M3<3`>m<)qf67_Pcb0eceX~?Z*>>3RrKpE=jo6
zC&1qN`T7>0xd--twYtx#GF6s$Q_1VD^K(pi<f1Qh^-oGq=$l;oCcX4l$!Xi`OBZ~K
zm9(;&6Tu`XxNON~Imhr*J9=(CEctz1<?pN2;;qJuj=%8x3qonJN0!)hSGzt7XPotT
zzvTYSs*XF#4#nzh&X`_#u*AQ`_JG9v{GN|L-)!94zAE(Hx&6G{CFZxc2)y#phztw4
z%e$mS+O%`N&i%^?+AEkF^p7*w?_>OD!&TwGVn6eT0-F#1<_GM1nf|>ri~hzu{rj=^
zE_DZ{e4Fod&yrbH<WkK3DRS5DR&I=39TNCI?^4?=M@bd&Xxq(k9yhI<k`LvU`gNT)
zys9bMJNx48oA2Chv&@>l-Hdo8_TyDjZ`nD%aOMleOT~7y$yLtR&z}~S9BzB}_WF{Y
zYN5_MSz4Q~>TU6quuqUX%*lUSY{RNoao4{Fb8Quu(KHminC4*BcxctsxZQ7=^0%CS
z_A>d4-S0*BpV&R@@IL--qkcg9yNi22&a`{}u5`U3pE*lW-?T>I%~=)??lu3_jcoL3
z)_$Gz<RsVmXg+s~s{1>$Yu0njHSfN_QU2aq$9_d>_4)1j-+yoam@2QUSNqd9a&Fcd
zzq2ns{N2oVzrI{%S;Z`+Vw0c7XIqSot(eZXG-`%R^c@!Q)!^a%wB^DFU7n97*DGf2
zx8@7BIlIi>%y(ZI%g=|q9~+4IZC>g)Z<^G;r3(u#1qCH&Z0$Rc*r(o{ssF)5x~i=t
zW1rj%ueFB@XFSrJBe_KL!UNW}l8j7!gDKzK9vF!E6*nKh9CFy)^vLB9Z_i-om8C3v
z$u_KPk29AoT{3gw6qD<#_U>Gml@AiFEH1Xu-7;s3!Ia5Py~{5M_$wF8*ljEMBy**$
zq3%RQ*;%~P+iDV7_>%kG_F2wy(p}r$)~DXGWe!VkxqFh%0x`CkP8t{1X7sEMxSpi3
z!Y$G8XjsCASI!yBm`zGVUH9d=-Jjvzb0A5Fy^1Y9Wn$fO_hoYG7ecl_zB0qV=Rne%
zpLZVoW|{SCm!xkko8e`9rP-2N32upoZqp7%i$=Yg|5V4fR%oGo)V__***s#&s>d#=
zL@)f7#>VTM!y1+0_?S7t@aVNe4_HsT&wKY}*@;X1y7#XvH03(2ecv-M-uB||UF+*i
z@2|_-KdJU=Nc@q!=<ENhk3OphwQbZ3Iw#KJU|{&?!~k8(ifuAR5V>uW3tx;3UDa62
z_2gOC^!XZGVgf7M=P7-?<h9pz-Co7KgKo!KZ0fo>1EX96`?Kpe&%0T=&(gHCz~#2)
zVs4?!9V{zaCwhgmR#w;YT~7(Ndy=+4oN1=XqWpl}8yt@}%ddPFk-BsZcTvH*REEO_
z7ZjHs3!C5)$R+CWuA(Bu!e-LuLlVUgeY>l&?6RjBTou0+&iZm~T3h+5<XPr74ApOF
z%+uYNJ?p2!<&!JJe!ZTy-{Q2<hwa8%e0O&3e)ovO#zcF`jt#l_+5Vo45szQ2Y@Tt<
zVDsZM|D=;smJ2+02-o)Vuza6<<kX$RqFGz+NJi&fZ9gi`f1qnwiKnoX?l!OQ%kTcK
z+8V9ftetW_>T~BIM=9NTRiUR1PCoQME>pLceS4krPhL;}JF`yJRbpgd@Mgjnz(}1Y
zBcx8#)iB@u+Xg&)--om4vE{J4Z@bLbdvVG1#M_lG&NV8X><frAQBn2#|5u~_=({;*
zZshLstm%KU*yE)C`R7i$eupABtAvl7)`;LZ+u%JnzbRh-{-NU!Dt|xZgmjyZqjZ~A
z6f$h!<Rh-zv}DCQt7AVOAa|RzA>F0`aJOmpgADX;Q`6ByOG;<%S}Qu=KmMcQ_0G++
zPk+4;7;`OKr{C==m!+~3r~f9ExMNEW-?N$ZVxGxszO@e~O*{Ep`TT<wA0xosrkyC=
zCQW#^sT$F35=ZVf-CSkRtPSfng<d#+`;Ao9hY7h}<%=2RIs{c?+Ad%G`zOM*V#(!O
zQ)kcGKYjj@+fMgS)@Hv--YA~-jp5<e5A7Cj-n~kz4tKLkWGg5WKDQ!ianK#P`KBu!
z|2i5fpT7D0&I0$RhhO|RsGm2j&!$ITGwSc#x^FZ7Z3+$AAGbee@7DQznjz(k-{REs
zIT|)>Sa_vEEMOUP+2qXAGB&QB8{XcV`)ub;yPql_KQ4$_blG+9r-fz*znA4tciC-`
zp%Zf}=;HQ*o`{lXWlI8j7A(7ec;{ipum;;o@vHIKhc>_Fjr`kd5jTC?rM-#I0>2bG
z%-R+(_xFpr-)$w{J!g2Evh2*0ZD*d?Ppn+fC)*}f|AV(Cb?>p?`jeHcPb}KLU2E-^
zkGJ-E*1k9q`1XEthv?gRjN$y#&TsZUZN<D^>B*J8Nx!?Y57uVweo|PzC~f+h^6RtL
zHR{_be)#<Rm~qq2K9+OGBDOy?3UPY=uEA1w@e=>5vnLrE?QGh^k-IHWveMiy<=6JS
z-_oEAU{Pza{s0pLgBTaS41m;oGSbJ=dwRd#z-Go`ok>;FcjbH<bc$xYNh}wGbe|@z
zSo&n!-u-nyC#2k(mTQ@LXlBB$#&;nbPbAfTO_-Sb<mvR<$TRmivWuejo_ol2CVfd)
z=A`hOum9ZN|Nk!6^Zjf7eRH~O(tpxu;m2(%q1i{bWc_?EIX~9)bVYNdw`T3!{9D`N
zZket1T)Iq0<8%&-!iJ?6_ROBRQALyO<K4XNH!SCB6udd(SJ1t7`<yp*uhQR`=UQ4Z
zy9K74zUa8+<a!<6xBqMYy^a6aHs!{t)ys~C`t)s{^m{Yg!zr6K?NsW|F}=gBzGcrY
zqv;z?NVgYF$V-}b{q5_T)2mdE`rgygj+vBp^O!ed_WP!#dV8nz1<Nd~dX=NN`n+!8
z?ww7A8THSaKOKL5pY627J>RRUDU~5FUkN=^xxC!E({8)!?~@9gk+pf3<+zL_6BTQi
zgfc%~Iq4KOzuMTdAzORbbiEfBJ*M&AoPH_ysBlYq&hpuBvJVv*wsfaXUv-O1ecArh
z$-MQaE9Ol%y}rfHwP9KC^#z*q+xtErxwh>5)V4V-->&TZy=+5JRqF3dzb?CXZ1O!$
zo-0Gm_5^KdxmdOG?6v8)#Vfx)tx6SIT$T53d8SxvquR@zpEkGnK5{JFo7x&O`-qul
zN5qPa51DQi@AdL$4d8k`YsL!CaOLZpC0D-OxNm!ft?l6@8`f#(NiCOk{_?&4R?-<E
zPTL!yxu;DNC%@*fkJJmAWnEQntY5D4JnzDh$Fm<9>OB(H$a`L!;=S--jooi;p?II@
zd20%yvOm7NC#ak9Y_p!$)@2N5!)w_aw(CA!?jjd0bR_NTq6hEyEZAYpy5Yv-*MH;_
z>eNhLuP|DlQjuO0Hz~dHG=GT2_Hg}gCuXe{-}+){Qw8&LS>>ataWX94U!?v{>3LXn
zxIE^wjnbO4p2ot{J}s5_dq{jmhU=0j-^044FSc2EzC0D8$N6N<EVD}Oz}%Z*TD1w?
z#&Hv^`PS#KJ~jM*`Ig}QV%53NTrZyH>v5d&<I(RG!73Bi87$qi=fk~qC;uNebqd(t
zJlFR2qnE9#vzr&)5=*(yYtOLab7;e}(3l+Iq})#`ic>`=FM7Z@<<X*t&*G2A$OkQZ
z^=6vjov0;iZaeQ!a{M5@(J1D-k<NLuwXLhyD0H@dUt(ERyz1z?9Y<w@%l3boKW&<`
z`9Y6Q%k(}R)cP<>WVxEC$>BXUxu<OGn%e~@K50>xSKipPLVCKau>H=Ct<M^2B!8@$
zpK-G>pFiEEu+lw!sb%)9%}bB2OwTOi*zj`N(e#4Hwf8dkn9PkIRsE=MH+=i|=|lND
zhyNX3e$MyvvQ@nQxYleu@Tm7*zi`yU>fb-)mX%9Sob1PxDDN`yh2f96b5tZZ&UoST
zboRvWpTBcte5qxgwXC83?@Wf)2YUr``JT=a3#(qyUiba>Lb;Q_OnhZnj!8Xvd}97F
z?)w#=GczWtzb{`uW6xV_^A+u<zMtqz`dPYD`S&Z;ZPF2!pBM-f`L7liZTYnP&QU%8
zBg&dRV(Y}GbM4_33}-r5BEIi2*SeZ-k$DoH@z1+m{Z~K8D|-0OZqH*TbKmv@MZGr<
zEI+z!%^IQWTYDTVoQ*H=zgnsKZvS61?z)-lCe8GlGk0Rqex)maTE$!UGTvdG<2GqZ
zM``iNeaEI&vE3*TK7LiXaf{Rn?o;`0f9}YOJ~<bZZ~G`M)v&JlQRhUJ9u9_rV6p6=
zqqBuJ>z{oTzQg8mjYC1%v0oL6Up@xCxZHX{ou%44BzEG{Bex#7nL5^(XWz<WTXWzL
zr!ueB1_!}cFYV;^xOTWbV(d_O`C#FcqU}M)yt(o!OBE&Ew}m%}2`sGkn#0Pqh+8+~
zA;Ur0I|@~c7w*>fe15Ptf6FKLvqgNz58mppzWVk?(&bIpgAQsJxo=k&oMvLEcVdC<
zvo$?N6SrNy+k0;A7ww>YNB8c$=yHke?+o(hnlJG=_9-Rgi2dmcLjN6aZqHe%Xt;Kg
z^lYv^xg3tm^ZIUy9hd%jV}g0PFL(7fX}xVrHmWW7|B>l$|8bFtnhV2rTKzZTe|YuR
zwb>fM>z7qt<ty)+_2GhNg&qTMI_ptu24P#iGt0RX>}*-ic)YD-GbmT)Z#us5XF=oH
z_Vx`w3nCvL-zYf!WIjuJdw0^Ef{HUcw>;Qd8N-#S&7XefmFraVpPRKyv)mjj9k*Or
z{I7G$Rz(ZNGePau#a7E^I9*IOcANRP?uu}gdWP)5pnSe^@z-07cUen6m}9*4&h<IU
zdOyD&y_EH)$N0}u$CjA#Js;%y%dJ1xEe!p6e{G3MyuV>w%I@hO!zRve;LLn<wI%Av
z?*nnaj=mGGxW#w8tLdcdr^Oc8QSZL7f3ui2C-{3t{E?Fp4*hLcrYOvQA|hec-Lma6
zuUxLfz02Brc0DMoGx}szE^BY|E-HYZ<=2gcxi!b*7!DL3Z>m!GaNIBWv2|bH?Or*L
zhK-lszBYbPyGZKb1Cv$vh1DgL?w9u663KNFXL5Y9%RRQsEM@vK_IuY7Pvz^GJm04A
z!A4hEHIwVafv>i*K915{0>1pa)*ha6IYDIRXDKH>hNzd}TNGpWN&oP;teWY(i^<pj
zgUJ5Mb(Y&(`HD=qRWmhi%DiBYiqrnpUMls)sW`59j)244l;ACjI?fW6Rhv9-P0@=z
zKlxAE1`n&cC+$&u8n-6saWIEp2N_mkyS;SAr|2h=CDANQD`snC1_%7=lYUjebt^>j
zqW6j7OJ~h1cI@Q)@MT%d#k7*j#^-Je>n4h9(cE1!d){O7<0<<bU;ON=58BOgI3W3u
z?bE7R+xil<{Juz3_PuY&{~#yOs&FMf#Hvj(H}8qnug+VBXEM0AOrNe$)%RX$^1jbZ
z>Q}12^d)KqF$plb_luk~D7n~pOPAg5XgP<Z&8wQaEiY9!CrfB0F)%Wi<jNkt&^$p*
z`Qqfh-3J!DXL|8_VcZd`HpTm{eeYk0ukA~GQE+wr$`9vcuTJ?c(`>u!{m1nl*+$lF
zE47}nDmYYWPUZ<dcUj*3VR4+Upuvx8JaaEF3SK$)bzZW^{C*~pxd(0)^1Qq(ENl1D
z^Qh^MMM6v>yQ+Sb@&p(B`V+ug^1W2X`B#kYRm+bu-zE3FbbR2b|K)4?!@gvX`QjhD
zIKS9004Z>a4gE34{@TF{OW19Xv(CF$`AsHS&V|F}UMIWi@d^7p_|Ltt?4R9u&|AJl
znZZ9Ux~gwsw!D2TvwwZn8_TvYFZH*-IJf!jT>oDy_`keZ^U%5EZu{%s{!ivld{z9z
zw)Efrb8G(bgIa5L^RJ8Ma56A#bHmqKL+TG2>5ujYDeDiyHjfrGedg^JVPF7Z(ALV3
zjMChsyu{3$V*L^rQ?DQ|y)(eiotH}rw4#RB)59f*fq~%$0|Uc<4rT@hh9%)I0vQ+>
z(gJ)!Tp1V`I5;?jgoLD|q?DDFb#--(jg76XtzBGPe0+R@gM*`@qLP!7v$L~{i;JtP
ztDBpfySln2Po6w`_Uy%r7q4Eudh_PZyLazCeE9I`)2A<AzI^-k?Z=NFzkdDt^XJe1
z{`~`4`v3pZbF=p{FbF^Jba4!+xb-%+yX=ld-&a5X7_s~B%{%}9Kg}ANdi>?tnS84)
zi)|u9`;vC&c<xaZ65qjcQ2d8)ynaB=o4V6mz5aIFpLnO9f9=nDe<S<dtNx$<9@lW4
zFNJ%9-M#(7^Z)(-vgogRI_r1+^DF<PZ&#}SdC$AvbkiiarT?TSXiW|>kkk?X(K<c<
zB*&}g|8;^j@Be>w)$-t@-p?P;A6%;PHPp*faK<#9eQf6EJAbH0di?sQcys$9k<Cxm
zMqHGf>SXNxMf=~gP$O4q_PiMaGgmo#U9-2}sHbhJwdXHyf)!)xRaPcXf!hsE7q0~F
za6R1ldxx|%i<EtX>ck&^xSQlRyC-<1{aKf_PIC{d_Ktrq>O<35y>_H5?K$^ycHg<f
zjr%RTSRPAqJZ?C_<nn^2p2@A}<jeOA-3}GjjVI^v=lnO+G5f8%^pf&VmK+m5hmTrU
z41136XKp`GCHf<L2|G*KnPRP#_Dr9hJr2)pb5^%WW>OAq_$G6MQ>TA%_%wTF=~b7`
z{R<1viIKV(vn8fTkM)AWl1D7NMf=|@)@Eu}s8}|Eui|u!*0BvI-_#`SDbW8Y`^xs4
z_Q$=!p{y0I@(n*rL{@2>?Ok<quLj3S_Ru303w}s9#cr%++V)v=)8_bNciz{OzJ9o!
z<=aw@U(eTn+|7_}(mZ*Q=el<_^-?EytnDw_SGV@SQQ`Ud35Vt%m}45ab%~Hs=hlZM
z{7sKeu6%LtmRf?E-NU<gEc5<`{rz{OukF~CGww?yU(Q_|Y^-6hwjpKb>(0pQ`KQ%o
z58Gd4&~CA76ue-WT_VROd(XjL&%xfcnBQha?18pRul;qrzsl^CQ#a^3(3N+|G-ylG
z%q=E;MG<kH4|nHy7$*KbeEmha?M2bp6!i@pOTWvk(S2d%uq}1p<D%2+8ei|0i>zsS
zuuJ>=om0O*{-1bUFCktwVp<i?%~c|QWWvAkFr1oJy+u-N_t6a*K{o_WyLlbDu<35E
zJJ(g-o4wy{4oh4X3R5rMW-1fi)2_<=YU8o368eiH_pH6om3+8tdzX9Cv7`-(TxU2+
zeg!p$7@e&Zs@}zV?5E9*r^n~;Rv(H^d|Xmw#}UQW^ZgSKTcWk&=EOC@rw@22p4O9{
zJ74Lq%LOC85`Lis8NRiX4{o{hEQt5k<jLJB@fGFowyg^1G3v2zT`RspAeuYqR7#7F
z>cI^!Sa!b>ShmKxL9_Aj&UIT2JrgfHS`)NOBts`;f5jW7Z=#J43$ng{jJ<WQy62Mn
zx$eVTMORqb3&(Ex#k}DM?;qXz>8x${+PZHX{_J}GaPis|#r`!%8nu5*&ZuEt`tHD+
zDeAYjy^xe;%nMsA7Rk2I|E}M(b8;+egWUde)z6y8zHhZHv;Nb4`(BjrrW!WMt@)KT
zZ$kXslI`W^7pFKrG5^na<}GWQOvsnwX~#~7XngvTdA+($>&@ZM4%4}6HH#MqGEG+T
zI{7O4?p4wKoDVhQr8iIFP`0d9+T-zM&a533Z<xv$f1hV~y~Za?I%>yz72eF#wmjj1
z9j0MfbC&;J@?h4}g!@~o-{%C`o-*NxXblsb`)`RWm)84>?+ke!W$eDbCTYbDnF*`E
ze}D4PW0^@n>+bCDDG_ZCQ|CUEx>_`0k7m=mVCjg`-*Z|w)zx?XZJv4l5(5)=P=v1F
zjkL@KN$L@Kiw|Dw{KjJNW69m=Yj%He7N1v|sNBC;Q2UnJ+d2Ur@iULU%m{xwbI+`@
z5aCOAKXXioJ|Fiw#<wlySIzNb(|lNWC-;=DE%okpio0?v(K#$Xb<4YRaku`mzTsxt
zEM%E{$9MX9{*?)rwY}y)Ns=(xk`>i;HSpRMo6YkM6#41$SQQ+ZJJUvY#g*F5l<Q0G
z3(VaXc)ej~#70jm{d?ZR1uO4OeV`nW{6;atyX=<dBu|x@(fbUqGILhVoII(@ZJvYA
z(}k6HICnW8dLXp;P8;L$#{x(8aqRkBGv6!f)&8W0sD9&#zh;TgSIV%RWA;qUdRK;x
zLWJ@*#^ln5Xc=8kz6!OEQy0v>_<pl4o6~B=d6~6hCPn)+18*vB_hjbbogBYsmN3)b
z>reM7&Rh``cj*A@8*Qf783Ng|i|xMr-uF?h;_N=FB<oAgvH32$=l_(A*ps**(`W9^
z>++Wl7+5FpCV3=HTkm?oCoA#hDzk-o0y9I@4VJA;T&a9gSX^4(c&)#e(9V!D|EPG@
zw6hUcY>qA1vODzT{@^!q&4+fE%|FL+OXTH>2hUBKMED|Zsqj|ZJ+VlLr&;{)Nu#F|
zKA$O1c<S@|u)mosTguE!4YLkBl1sRDrl!U8ZQX`0-RSG@H0MP=nEd=9-?SY|I<u~s
z2K34;5zF-s&$&P4lh67}qe)uYSF-lyhTnf;BW#xz{pI%Q?p5^>AO3f|2sv8+>dF5V
z1-BJ-rcIwdUFUzq@17f{PiOyszAF0qhp;D4pWb%8AiiNed(JHnO&8<-j5~8SzE*o1
zH)G+ED1$pJ`mQIgCYUQnS{Ad5HJwglnVI%w=F^@sMd^u)_5R&hq#ael^he3@_bpAy
z)tbc*I6{uUKhSq*t@-5Re2z9uvv1Wdck4+GpETo%M_<m_kKQ^LzV4{DoAcXq{?^}?
zrx!ih7`xluzirw~_Z?p{Q{3jU9NRBka?$yy;;f=&ff|n;j)(G0+J1t0YH3<XtoN!Z
z8->EYuKLqfn;TL$eTVImYm+7$-#+YoA@_l`)s_WZFLXaSgcQb=uWfbPzHWMLf@<od
zOEETOjK8Z6Xnjl9zG^9ODDAD?Ly67ZheeM^tk1HXy6W+VQxEypOu2Mf!FOr!{&qQE
znT=_?yuZHKBmDZ+MzO<3om?-kj%0q-u;?D=E#b8~uDidMt(&A!_%C_d+sp54rO)aW
zC0!Mp7m@b0o+FC8kIiyMeR~;y<JWgTlnm4_9*my1Mzvn;1%p*oL7A4K%v{OjZH%ka
zJR0ZLu4Gr}7Bsx(I^A;ZCx&GgAFfg4=$Y3l#Wm-Os)y|lv)73&?^YLA_%4vvJMzfl
zeN&glihZDBk+pHIh}nZ$!@9dG?>e_{tl9f<XV}?Goqvrtlz2a2SzWMvdwbdbm2IsH
zTi2=i_lK8UJ}GQ@aN_FS9|fdNT5OM$T~>Y~>(cBX6|SY`ncrV<Z@DMF`NdQp)_E%z
zB|cJq|Bs>a`n%(2H=Iz<f1JN$i-URQ_dUfLDQ{n@XA8ebH<?~^=981X2eXK^is<&;
zW#?r-*xssL@aXDy*SGUdHK$g%l{|dAamvSe*Pe5pce`k0tIK>uM$S6J`kT&uNgJc1
z;k!c~b=d}%AMU=KS>@Q>YL>kv?0BtdP&?aV-kR5Q<nN@2{{FPo;7W%7%xCiHCi+eP
z^4YJ|hbO50z0PdxR(aD%XbXGt(V2V?MZJG~Tej!-Oz+ksTS_MN8D~ZDMk@q5u=H=)
zr{`?*e1YS{Lp+~&t2i&~-<(o@f2FFdSornmr6Nndmhf<CUAsM>W7m0=f5)Hvx;M+x
z>e*M-`RpIQPV`%l{kzh$?%}dY2TZw_v==ThKQ6Q~ddey{<(I1~zu&UhIPaSIrDz_v
z`?0HdO25pi(XbU+!6=)UvGL2#*gHuw*%<+0$`hu{n^7)vuzlhuaCYK2WBx+TVek1>
z&KAknb^Qv$qqZhoYs)@jP`)j_H04#$mM--TU3Il=?uK%!jV@We{dB_WyUi!LnY+!O
zg+wZEx;R-WRBu-QsoRN8`_E^{^=WkaxgXkL8En`o)nPBgtFpmXFS(@nRo%xWk&DV~
zTjX5~=gG0GJ-4W=lI;Wg+bw4o9aeWdo@-jH6}bKAC8HZE=fb58A`S+8`g~|dv8Hl_
z@`dZO^rlWooBgb@&qq7?;_{%)Y<IJ^{Y&6I6k}!3s9CVJ$~p2#gv^~Yix`zt123Ij
za!{7#?E>zNE0(NebX-%n!D5Qbvp=VH?{BCLO_={C?Dk6Dp8q#IKN$Z05V<?NiBI!J
zd1k^6-5oQMV)fb-Iyq<G53}v}W9^@Ezqo1XvuV?<x;Hmne>7+Hg)SA%w{magI_F>C
zrFHkY<LcO}-qlAp)PHF=VK7?ud(t1RlM7$Y@D-HaT74@0(vMq~PZi{*H6{jVE6(Hp
zW!qiNwAxMkXQb4P$CV<STDs2?&%JT`B0g<*QuE5L`i$={f?SolH>@%A-p%^xo=xeN
zNxHEUD`vgT&2>AWrK}WvW_zm>uc6c3=|<Nq3vXnftUdEXmY*jfOMda3(;a0JM~&R{
zy63sCebKIa-Q@M=pI?<;+-JS<V{Sv`xm}OHANZ7)dU#v4#zO1o*(vds+BcS6H8eAK
zd-y2t-P)^xX6)y7Ufy>u>U&`1_O+8DL=V(P_AIEBz0w%38!COS*H4b+ZcG2Oo{Q(2
z?Zhfh$MUb)cra*TcJ7p&cMq(&uBo?3=E~vasy}%uE00b6-?qhWc|_B;XF6q>FC-E}
zKlUee7}d>)F;9<O_&$|m>K%(ot*acubA>`Ti?84NY>Qugg<R&f-TL=-zL~50BI4(r
zw52~ctbLIFQFc=Nn@~lk@2mGE6<_PExC)9q&xDPQrprXC%fk+zOp^Z67`aXEZ2lJR
z>$9G&{rDp9rss)mj|%l8?^a2R$~bNgbWM1AV4?Y{b9?)Eryluodxrakm)FnMipuaa
z>YP6MX8Wnr6J6?b#J9DJ{S&dA<zinrEA>&IWPdAf@Yc^o#v1(G)2h=R_<F}bDf;^5
z$dc{6cG=%wPMO-?vB9)yp0HU(i0<`<v&tVr6Ydr~<N7<<#9+GQoNQscE!8{OC1e+_
zS@QMlnM#&r(=Y!jVo`hCyg+qF&>Te_KF+5COx8=LDS2o9zJLAQ(}UeME>R!f8QYf}
zI{fkKo&SyZY~?;a+Q@z5I@`71`7A!gmlXCND$h*l&y(NB`(eGZ?45Np7$jmCV(00~
zOyPEyds;G8u<ts@x&F=5)`yz>jMPu>HVK$8=i`Sm$6q<A=iVx9*mSF<ZOx*;%1>WN
z7^(5TTKjtDCIbx*|AXrUUd0QS1eG~Hw&R@DT#~bMpVHKSaogU-N@Yld-hYxkL;Q{w
zuZ<0VMCXG0w*5~zcJa?RbglgDK8>Wx8Rp*$ekd=RK4aU9ZvyvXxXtr-{QdfJT3Ua^
zM}<7o_xl!1UVY_p=hR4MF5csB&WqN++WB?j?`2U*noIkRuh34`S!%<7;`IDne~Trj
zL1m9Vhfcvg<>|_{Yc}265}tc7!<GB$Q7?lW6RGrRO)-A{?D-CMd#a!N1l@fQ-lZbz
zw_0YaN8D20%J1{~9yVz2UvT&Of%LuAUemVzjtsj}xnsGE?AtZv{5qQ>_te^LbZnSc
zeKoIZfpqS1ufW~E^V+X{c$yj~@rU#1Vf7|C9e%U#-HSJrYum7dRc!YT?Nc*IHh30y
z_1)YJEl=gej%|#vKCKiU<hCn6ZpYGlwsGs_mr4cK$4W_bnl8^$zN)J?HN(<i{ioQ^
z922U~Uz>3!SL)adxdmsczL&Z0{k<~uk!f_q4v~2e78&ll`Ss-Si3+>2wfAt}n9d@$
z;CJ<bS?Ba;7qK7O`}q0PpBv3OHNFc@6W=a!|HF>+{a+2QUu>#oo#iLHab^o&y>Rq|
zmoxY1MhJbpezx{;u)*JH6%o2m;v=n$`ul66&n&E5(WP|x%&Q6!WyQP|H#alB@6kWJ
zX6}9Q%AV{VhiTKF^gE?~khR-Vt(q3LFzwmCWSRThlVzl1dH8CVuH(1jFuS?a`CO6B
zGK=k<b>D4Nrmwd%7k;k3+J<@gHb!r!J;#=YOgZOxvRU^zkAvrdl&T6jrX0=U+bJ8I
zcsr**Iq7ln#kAOUPkX~9PEBUzRo%?2xU+_1pT#k&=bO0S>C5eIsLf5N{o{AwRc_YP
z<!^Uof3G|JRat1ugvrzE{#G%sR4abCaPK;{3;9l>$KD+~Eb&rM;P{H2elf+CbrY(B
zqvD<9W><bsObl9-TKDYkc{ANAxlImL>kk-Bf1;i%eDB^Rn^Z=_?ESe{-mP2^d!+TI
z^cR~`j!oS;q7vJWGyK(D>wo7<_MB{U|F`#wRQ~23=wkS)_G4Dr`P&w8Utd=((R>xl
z|N92l`pbSyWlk241T#|-{U4tAA;#so<;#cHfpwo%GL5sv*DYg86XR2U6ub0P!0!Ve
zLlzvb(mQ^9{>R;0*dsXh9_`<2S;rf3pdwZ8WP9rK<;Mb@Jj5O25A2iM5cytCH!-<?
z>YCl(R;{)8x3)mx=%KATZLLk)_r$%AE4<yhBfnLAkLzNIC%>&;T;7#2u~|=gOSQZE
z)9$bDRzFwpN-x=YulB2hOPzjJ_`UC|Lgzd&Z|t%9zRLFX-Ta9=1SQ<f+tz-JkTw6c
zV)HJc2@8LR9h;x^jK^xt?Korhj}o39ku2ACD4iGil)r@IYh~h{fQ6Ioy2B=i9lKb5
zb@zN}qgQT^gGxINRrxq>-W2uTuG6ii=lh|Faw~VJFArIjzW2A$eZz&Wf6o2Mb&t>v
zoxE;C(0OI;)b_#;F1Gy(K5zI2DyGC)+RkOwc6^)gZR#%f<GbeC#D_n7={@JP$Hu_Z
zejhsi7OobTc)nkx^1`<}*2M}-d(*cC|GoK|!##Za#GU_3y*^#~bc&VZeE9cOOC3d?
z$=}**XVUAD>u_Ew#%J;gQ`2g%m)|6fHZA<*H0ef+mHh;7PMvpmxIJ5!CG9xBZO_4(
z*QUR*`1f4?ug`04>C3-9{5o;=hG>}96-(=#m3KdPY!_F`)4y;2P`4_LJD}tFl9o>;
zv&-sV@xQoqq?N0*mg{fswJqM=uWADi9Nk@Z{=k%^w293JB<-pdGcQfrp4`s)a($C{
z<>OY}6Zu(U6O+t)-$s6Yw{${3>mKp`*aLbA;v2Ycu!4HeyBny?ogM$5`?IL*(jx!J
ziJ&v?JYD@<);T3KLC&$mwqi(>fq}u-HN;WZ)6Y#m7j_m}MQ+a4(7k!h1_Jj!i=4=A
zy=xE}=F#RAyL$=$gBiv<jJ7?UuTlA1ilt>$m&mFOH}8D>JD0Dl-Fx*WV+;LWy^CV|
z7x9>wPrXvwxvx+Dr?k}@^WD=jH4m^`$!+>F@7v|AE*CSiW=x-#b**W6V{o!#c-wKY
zk_G#JXP!5?o5sXt;-JkuUGVzV5*8t~S6!`FYy}P;ZJHe0shQO>LFNU|!t`7Dn`W~r
ziauF+H#VQiB}8kxj)|&LdFfrJ2Cq#vF}hPaB3G-tXPvltUBP_DdC|x3StU%(XJAtD
zUb00%!Y}S!KzmAm$y3(_@7=f~-LHFpW39X}y?@u_ro~5U`Zip+_<?7)myN@mU2$U4
zKA)V#e{XL7EZ`Ky{lDfxLFk8?8|N>Zf0&Sa^45=RRy)Bpo7jba{TH8YenvOuW#iU}
zN{yqpoHfH_PaTe5`kd$KjU(Td%nX^=^08y>y7wIubXPZ)d_A&Bx&B}8Z+XxlKD&7A
zlmtcwhA?)}AU-3L2!jaD<0?VXiNLVKD+9bCx?oX@eB>eMKuUy;5C#SY*bD$n7X$QY
zOoS>1@NtL;J`WSV!x15NV>3ktVFUvMgA*20P!CJQZ4&5gKZId5SWH4bJQ24!s4m)q
z#hgTx!xV9w1RC>4xab`glMsh15^IVIGiEr04ljfpwusvl)X<5-VhZx%i@41J9lwb1
z(<ChBWTGF&h}$q!N1exFSOL=Ej1Y5R2^jh0LD10>2uHEAFfhOisG^iKSR#h$L_V$p
zbTT1AryDEEIfdvNOOQ53qgv@L%)o$rwgtLQ<c(IKX&!`?Qj!b|h&@&4`j9uOfL0VD
z^sy*1VB3_1ZUFLXP|%7jgaLn)kqkgupM`D$@^VMeEFr>#8#+iPpqCi1z(!syhUx=L
zJ-Bw{6_V)oBhO!=`oPK%$pEr^@WKko1au$3N-OkPJVXF^+AuKSn$tt~2671ws!9>2
da0TM1SOdIS*+9y~8N?Z0vNABN1x*Yx003+sADRFF
literal 0
HcmV?d00001
diff --git a/learnlib/GraphvizParser.java b/learnlib/GraphvizParser.java
index 81144c4..8a2e8d3 100644
--- a/learnlib/GraphvizParser.java
+++ b/learnlib/GraphvizParser.java
@@ -68,6 +68,10 @@ public class GraphvizParser {
}
CompactDFA<String> createDFAfromMealy(List<String> accepting){
+ return createDFAfromMealy(accepting, "0");
+ }
+
+ CompactDFA<String> createDFAfromMealy(List<String> accepting, String initial){
Set<String> inputs = new HashSet<>();
Set<String> outputs = new HashSet<>();
for(GraphvizParser.Edge e : edges){
@@ -79,20 +83,20 @@ public class GraphvizParser {
List<String> inputList = Lists.newArrayList(inputs.iterator());
Alphabet<String> alphabet = Alphabets.fromList(inputList);
- DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0");
+ DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial);
for(GraphvizParser.Edge e : edges){
String[] io = e.label.split("/");
for (String o : outputs){
- if (e.from.equals("0") && e.to.equals("0") && accepting.contains(o) && accepting.contains(io[1].trim())) {
+ if (e.from.equals(initial) && e.to.equals(initial) && accepting.contains(o) && accepting.contains(io[1].trim())) {
builder.from(e.from).on(io[0].trim()).to(e.to);
- } else if (e.from.equals("0") && accepting.contains(o)) {
+ } else if (e.from.equals(initial) && accepting.contains(o)) {
try {
builder.from(e.from).on(io[0].trim()).to(e.to + "_" + io[1].trim());
} catch (IllegalStateException ignored) {
}
- } else if (e.to.equals("0") && accepting.contains(io[1].trim())) {
+ } else if (e.to.equals(initial) && accepting.contains(io[1].trim())) {
builder.from(e.from + "_" + o).on(io[0].trim()).to(e.to);
} else {
builder.from(e.from + "_" + o).on(io[0].trim()).to(e.to + "_" + io[1].trim());
@@ -100,7 +104,7 @@ public class GraphvizParser {
}
if (accepting.contains(io[1].trim())){
- if (e.to.equals("0"))
+ if (e.to.equals(initial))
builder.withAccepting(e.to);
else
builder.withAccepting(e.to+"_"+io[1].trim());
@@ -111,13 +115,17 @@ public class GraphvizParser {
}
CompactDFA<String> createDFA(List<String> accepting){
+ return createDFA(accepting, "0");
+ }
+
+ CompactDFA<String> createDFA(List<String> accepting, String initial){
Set<String> inputs = new HashSet<>();
edges.forEach(edge -> inputs.add(edge.label));
List<String> inputList = Lists.newArrayList(inputs.iterator());
Alphabet<String> alphabet = Alphabets.fromList(inputList);
- DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0");
+ DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial);
for(GraphvizParser.Edge e : edges){
builder.from(e.from).on(e.label).to(e.to);
}
@@ -127,14 +135,18 @@ public class GraphvizParser {
return builder.create();
}
- CompactDFA<String> createDFAAllAccepting(){
+ CompactDFA<String> createDFAAllAccepting() {
+ return createDFAAllAccepting("0");
+ }
+
+ CompactDFA<String> createDFAAllAccepting(String initial){
Set<String> inputs = new HashSet<>();
edges.forEach(edge -> inputs.add(edge.label));
List<String> inputList = Lists.newArrayList(inputs.iterator());
Alphabet<String> alphabet = Alphabets.fromList(inputList);
- DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial("0");
+ DFABuilder<Integer, String, CompactDFA<String>>.DFABuilder__1 builder = AutomatonBuilders.newDFA(alphabet).withInitial(initial);
for(GraphvizParser.Edge e : edges){
builder.from(e.from).on(e.label).to(e.to);
}
diff --git a/learnlib/Kiss2Parser.java b/learnlib/Kiss2Parser.java
new file mode 100644
index 0000000..3548bfe
--- /dev/null
+++ b/learnlib/Kiss2Parser.java
@@ -0,0 +1,78 @@
+import net.automatalib.automata.fsa.NFA;
+import net.automatalib.automata.fsa.impl.compact.CompactDFA;
+import net.automatalib.automata.fsa.impl.compact.CompactNFA;
+import net.automatalib.visualization.Visualization;
+
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.*;
+
+/**
+ * It is *not* a general KISS2 parser, it only parses the things I needed for the mealy machines.
+ */
+public class Kiss2Parser extends GraphvizParser {
+
+ Kiss2Parser(Path filename) throws IOException {
+ super(filename);
+ nodes = new HashSet<>();
+ nodes2 = new HashSet<>();
+ edges = new HashSet<>();
+
+ Scanner s = new Scanner(filename);
+ while(s.hasNextLine()){
+ String line = s.nextLine();
+ line = line.split("#",1)[0].trim();
+
+ if(line.isEmpty() || line.startsWith("."))
+ continue;
+
+ if(line.matches("\\p{Graph}+\\s+\\p{Graph}+\\s+\\p{Graph}+\\s+\\p{Graph}+")){
+ int i = 0;
+ String input = line.split(" ")[i].trim();
+ ++i;
+
+ while (line.split(" ")[i].isEmpty())
+ ++i;
+ String from = line.split(" ")[i].trim();
+ ++i;
+
+ while (line.split(" ")[i].isEmpty())
+ ++i;
+ String to = line.split(" ")[i].trim();
+ ++i;
+
+ while (line.split(" ")[i].isEmpty())
+ ++i;
+ String out = line.split(" ")[i].trim();
+
+ edges.add(new Edge(from, to, input + "/" + out));
+ nodes2.add(from);
+ nodes2.add(to);
+ }
+ }
+ }
+
+ public static void main(String[] args) throws IOException {
+ Kiss2Parser parser = new Kiss2Parser(Paths.get(args[0]));
+ CompactDFA<String> dfa = parser.createDFAfromMealy(Collections.singletonList("1"), "s_2_0");
+
+ Visualization.visualize(dfa);
+
+ CompactNFA<String> nfa = FSAUtil.convert(dfa);
+
+ RFSALearnAndCompare<String> learnAndCompare = new RFSALearnAndCompare<>();
+ learnAndCompare.setTarget(nfa);
+
+ learnAndCompare.learn((int) (1.5*learnAndCompare.target.getStates().size()), 200000);
+
+ NFA<?, String> result = learnAndCompare.experiment.getFinalHypothesis();
+ NFA<?, String> result2 = learnAndCompare.experiment2.getFinalHypothesis();
+
+ Visualization.visualize(result, learnAndCompare.target.getInputAlphabet());
+ Visualization.visualize(result2, learnAndCompare.target.getInputAlphabet());
+
+ System.out.println(args[0] + "," + nfa.getStates().size() + "," + result.size() + "," + learnAndCompare.experiment.getRounds().getCount() + "," + learnAndCompare.mqOracle.getCounter().getCount() + "," + result2.size() + "," + learnAndCompare.experiment2.getRounds().getCount() + "," + learnAndCompare.mqOracle2.getCounter().getCount());
+
+ }
+}
diff --git a/nfabenchmarks_pgf2.csv b/nfabenchmarks_pgf2.csv
new file mode 100644
index 0000000..fbecea4
--- /dev/null
+++ b/nfabenchmarks_pgf2.csv
@@ -0,0 +1,8 @@
+file,origstates,forwardstates,forward rounds,mqueries,reversestates,reverse rounds,mqueries2
+Ba4bPa0,4,4,3,174,4,3,145
+Ba4bPa1,3,4,2,27,3,2,21
+Ba4bPa4,16,16,7,3616,16,6,2260
+Ba4bPa6,40,36,16,23120,36,15,16473
+Ba4bPa10,125,88,43,305493,90,35,187889
+Ba4bPa11,89,67,26,136359,61,27,91485
+Ba4bPa12,165,101,57,448655,95,49,247566
--
GitLab