From 2abd99c70b29f717c49c1b08419f5ebc1480a040 Mon Sep 17 00:00:00 2001 From: pimjager Date: Wed, 20 Jan 2016 11:04:52 +0100 Subject: [PATCH] Added exercise code from BB --- a4/code/src/CandyLearner.java | 213 ++++++++++++++++++++++++++ a4/code/src/SutSocketWrapper.java | 93 +++++++++++ a4/code/sut/CandyMachine.jar | Bin 0 -> 14192 bytes a4/code/sut/learnlib_dot2jtorx_aut.py | 181 ++++++++++++++++++++++ 4 files changed, 487 insertions(+) create mode 100755 a4/code/src/CandyLearner.java create mode 100755 a4/code/src/SutSocketWrapper.java create mode 100755 a4/code/sut/CandyMachine.jar create mode 100755 a4/code/sut/learnlib_dot2jtorx_aut.py diff --git a/a4/code/src/CandyLearner.java b/a4/code/src/CandyLearner.java new file mode 100755 index 0000000..7b08a7a --- /dev/null +++ b/a4/code/src/CandyLearner.java @@ -0,0 +1,213 @@ +package nl.ru.cs.TT1415.assignment3; + +import java.io.BufferedReader; +import java.io.FileOutputStream; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.PrintStream; +import java.util.ArrayList; +import java.util.List; +import java.util.Random; + +import net.automatalib.automata.transout.MealyMachine; +import net.automatalib.util.graphs.dot.GraphDOT; +import net.automatalib.words.Alphabet; +import net.automatalib.words.Word; +import net.automatalib.words.impl.SimpleAlphabet; +import de.learnlib.algorithms.lstargeneric.ce.ObservationTableCEXHandlers; +import de.learnlib.algorithms.lstargeneric.closing.ClosingStrategies; +import de.learnlib.algorithms.lstargeneric.mealy.ExtensibleLStarMealy; +import de.learnlib.api.LearningAlgorithm.MealyLearner; +import de.learnlib.api.SUL; +import de.learnlib.cache.Caches; +import de.learnlib.eqtests.basic.CompleteExplorationEQOracle; +import de.learnlib.eqtests.basic.RandomWordsEQOracle; +import de.learnlib.eqtests.basic.WMethodEQOracle.MealyWMethodEQOracle; +import de.learnlib.experiments.Experiment.MealyExperiment; +import de.learnlib.oracles.ResetCounterSUL; +import de.learnlib.oracles.SULOracle; +import de.learnlib.statistics.SimpleProfiler; +import de.learnlib.statistics.StatisticSUL; + + +public class CandyLearner { + + public static int sutInterface_portNumber=7892; + + /* + * The Adapter: needed in order to let LearnLib and the sut to communicate + * + */ + public static class SULAdapter implements SUL { + + // system under learning + private SutSocketWrapper sul = new SutSocketWrapper(sutInterface_portNumber); + + // reset the SUL + @Override + public void reset() { + sul.sendReset(); + } + + // execute one input on the SUL + @Override + public String step(String in) { + String output = sul.sendInput(in); + //System.out.println(in + ":" + output); + return output; + } + } + + public static void main(String[] args) throws NoSuchMethodException, IOException { + + // create alphabet + Alphabet inputs = new SimpleAlphabet<>(); + inputs.add("IREFUND"); + inputs.add("IBUTTONMARS"); + inputs.add("IBUTTONSNICKERS"); + inputs.add("IBUTTONBOUNTY"); + inputs.add("ICOIN10"); + inputs.add("ICOIN5"); + + // Instantiate the sut + SUL sul = new SULAdapter(); + + // oracle for counting queries wraps sul + StatisticSUL statisticSul = new ResetCounterSUL<>("membership queries", sul); + + SUL effectiveSul = statisticSul; + // use caching in order to avoid duplicate queries + effectiveSul = Caches.createSULCache(inputs, effectiveSul); + + SULOracle mqOracle = new SULOracle<>(effectiveSul); + + // create initial set of suffixes + List> suffixes = new ArrayList<>(); + suffixes.add(Word.fromSymbols("IREFUND")); + suffixes.add(Word.fromSymbols("IBUTTONMARS")); + suffixes.add(Word.fromSymbols("IBUTTONSNICKERS")); + suffixes.add(Word.fromSymbols("IBUTTONBOUNTY")); + suffixes.add(Word.fromSymbols("ICOIN10")); + suffixes.add(Word.fromSymbols("ICOIN5")); + + // construct L* instance (almost classic Mealy version) + // almost: we use words (Word) in cells of the table + // instead of single outputs. + MealyLearner lstar = + new ExtensibleLStarMealy<>( + inputs, // input alphabet + mqOracle, // mq oracle + suffixes, // initial suffixes + ObservationTableCEXHandlers.FIND_LINEAR_ALLSUFFIXES, // handling of counterexamples + ClosingStrategies.CLOSE_SHORTEST // choose row for closing the table + ); + + // create random words equivalence test + RandomWordsEQOracle, MealyMachine> randomWords = + new RandomWordsEQOracle, MealyMachine>( + mqOracle, + 3, // int minLength + 8, // int maxLength + 1000, // int maxTests + new Random(46346293) // make results reproducible + ); + + // create complete exploration equivalence test + CompleteExplorationEQOracle> completeOracle = + new CompleteExplorationEQOracle<>( + mqOracle, // a membership oracle + 5, // int minDepth + 7 // int maxDepth + ); + + // create equivalence oracle based on the W method + MealyWMethodEQOracle wOracle= + new MealyWMethodEQOracle<>( + 5, //int maxDepth + mqOracle // a membership oracle + ); + + + // construct a learning experiment from + // the learning algorithm and one of the equivalence oracles. + // The experiment will execute the main loop of + // active learning + MealyExperiment experiment = + new MealyExperiment<>( + lstar, + randomWords, // equivalence oracle, choose among [randomWords | completeOracle | wOracle] **remember to change their settings** + inputs // input alphabet + ); + + // turn off time profiling + experiment.setProfile(true); + + // enable logging of models + experiment.setLogModels(true); + + // run experiment + experiment.run(); + + // get learned model + MealyMachine result = experiment.getFinalHypothesis(); + + // report results + System.out.println("-------------------------------------------------------"); + + // profiling + System.out.println(SimpleProfiler.getResults()); + + // learning statistics + System.out.println(experiment.getRounds().getSummary()); + System.out.println(statisticSul.getStatisticalData().getSummary()); + + // model statistics + System.out.println("States: " + result.size()); + System.out.println("Sigma: " + inputs.size()); + + // show model + System.out.println(); + System.out.println("Model: "); + + GraphDOT.write(result, inputs, System.out); // may throw IOException! +// Writer w = DOT.createDotWriter(true); +// GraphDOT.write(result, inputs, w); +// w.close(); + + String filename = "/path/to/yourfolder/CandyMachine.dot"; + PrintStream writer = new PrintStream( + new FileOutputStream(filename)); + GraphDOT.write(result, inputs, writer); // may throw IOException! + + System.out.println(executeCommand("dot -Tpdf /path/to/yourfolder/CandyMachine.dot -o /path/to/yourfolder/CandyMachine.pdf")); + + + System.out.println("-------------------------------------------------------"); + + } + + // execute command, for translation from dot to pdf + public static String executeCommand(String command) { + + StringBuffer output = new StringBuffer(); + + Process p; + try { + p = Runtime.getRuntime().exec(command); + p.waitFor(); + BufferedReader reader = + new BufferedReader(new InputStreamReader(p.getInputStream())); + + String line = ""; + while ((line = reader.readLine())!= null) { + output.append(line + "\n"); + } + + } catch (Exception e) { + e.printStackTrace(); + } + + return output.toString(); + + } +} diff --git a/a4/code/src/SutSocketWrapper.java b/a4/code/src/SutSocketWrapper.java new file mode 100755 index 0000000..04ffd46 --- /dev/null +++ b/a4/code/src/SutSocketWrapper.java @@ -0,0 +1,93 @@ +package nl.ru.cs.TT1415.assignment3; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.OutputStreamWriter; +import java.io.PrintWriter; +import java.net.Socket; + + +public class SutSocketWrapper { + private Socket sock; + private PrintWriter sockout; + private BufferedReader sockin; + private int run; + + public SutSocketWrapper(int portNumber) { + + try { + sock = new Socket("localhost", portNumber); + + /* Call setTcpNoDelay to improve communication performance : */ + + sock.setTcpNoDelay(true); // remove unnecessary delay in socket communication! + + + // make char writer from byte writer which automatically encodes chars using UTF-8 and + // automatically flushes the buffer on each println call. + sockout = new PrintWriter(new OutputStreamWriter(sock.getOutputStream(), "UTF-8"),true); + // make char reader from byte reader which automatically decodes bytes to chars using UTF-8 + sockin = new BufferedReader(new InputStreamReader(sock.getInputStream(), "UTF-8")); + + + run=1; + } catch (IOException e) { + // e.printStackTrace(); + System.err.println(""); + System.err.println("\n\nPROBLEM: problem connecting with SUT:\n\n " + e.getMessage() +"\n\n"); + System.exit(1); + } + } + + + + public String sendInput(String inputStr) { + try { + + // Send input to SUT + sockout.println(inputStr); + sockout.flush(); + + // Receive output from SUT + String outputStr=sockin.readLine(); + if (outputStr==null) { + System.err.println(""); + System.err.println("\n\nPROBLEM: problem reading output from SUT: SUT closed connection\n\n " ); + System.exit(1); + } + + return outputStr; + } catch (IOException e) { + e.printStackTrace(); + return null; + } + } + + public void sendReset() { + + // send reset to SUT + sockout.println("reset"); + sockout.flush(); + + run=run+1; + } + + + + + public void close() { + /* + try { + sockin.close(); + sockout.close(); + sock.close(); + } catch (IOException ex) { + + } + */ + } + + + +} diff --git a/a4/code/sut/CandyMachine.jar b/a4/code/sut/CandyMachine.jar new file mode 100755 index 0000000000000000000000000000000000000000..e78003bf7ee42ca007cf004aace98559f36a93eb GIT binary patch literal 14192 zcmbt*19YBS6KZoxUtdLHk+iejRuWv+qR9Hob&&GdwO*5y0g}|@+O&? zZ_nO)u=o3nwAkBs2mqj1sLIo@aR$Y$AGE-+WQx1WJ{tPH{%*b-64x6_PO1 z9a7-E4q4HfNiC59!LcAep3K#83E5rQm4x{^+@M6NRw!VG& zuZ7u%zh?mcox$4fA9%q2$D?QS4{WeMv&qZT(9huzQ0bZJ*x2|+YKQ^yAovaE9c~%A$6V;oXOW(9wuqxI^p* z0mq)n&ro~=S@*gGiHzXuOLvCmT7L4VX#BR+M(Ru!Mod9v?FnLwSuo<|G}G$Utfv#_ zd!mi#Ml_K$Dyp<|Tj7Q7`t*qJlQ}Ct3teb7qj4zhUJ?reJxI<>Z){tXnzcik@y>}( zi4KXPx)ob9OnY$~GfO73-FFU_1UaU!Xa_ z6^zbzW_AeXbt?igJ0+{X0RR|zai72U9HxI+Ha;B-eJ2SWJtJca0|N0+dOANAFg0dY z7F`Iz@0kaXfw!gX7#I=-%*+S2kdT`~7f}qhOD07E6g4;ica-W2Y{Q&$1ZLCcgE28?9fS3HG$DQ*xmv3qxx8lFMyMp5cl#;FTkA?DOsn6Kp z9(EBNS!0lk*YB=z97W22(nuk+4LBeeCaUE=+W&MPMQd#k&KKiBa{`&gux+mB(FXtDQ8p&}* z+#M}ZRUw#~sC*Yx^2O(24BSLJL2FrSQEPQ;UTbk$5*9L4>Xj@EN}hRTu-5loVhJQV z6+ZdzbHozhLSp^GPX|VuINp{#dHc>38!fclq>7p6t+6Lko;is-yTvEB*4x_0FiN9; zy*gam)nTpu!ag7yES9rWZ>l|s&L)yZ{5YFscMy(jjk?dg(Xe3Mj!G_M4P#arpd zY3_W5&h@Ab85r>So)c@KD;|sBBq@w^;R2@vZYyCkVLf3xz>>m}!kWU0!iJwkky(*t zig}8Kk(rT27eftW9)k^|q0Tsc>vo)0I;}5FrD{{K^tesr2qP^^4u}=$*kduR*c71XE*ZO|?`Fchp5J`EwFgKJs0sGh<>{_UGmlzK3b+|;&w|(ICQ~Zyg z))f}N!x)UIP6BL?z>s(VZwJ5atFt6=;%36Q08-~`PnD8BU4%$ImX2GsBWdIzbs(M3 zRj}?}_VA*UIksl^bPf@PtCh4IAgGGqw2ae9(eGdeWoqjK2GTM?6j8Ac)+EysNAp=JP(T7_>uj*Y~L^*cmNKUeQit5o3CIU!XZQw+!8n#jZg-Z!3M#Ll&2fm zYn{otSoD!b>?lolOsMP0#(aEy;xKNN_k;JE%lC#?*UQIT07dQnZEcH?;uIvx@@4uu zED-2nK-0W3E$s2tIUjKP0B`ALBXZpjnEF;DpA~Tk$*rVefROCllBSKEV|(V8KbXfH zInB!;$hXUJg-kb@56%&Ikb`>P;3^zi&$7T$V@-#Xa8|+lJXLP(W-QOd`!gtFyuTZj z$J;Hy#;(#JGWX{cQg$5GV`!hV?>>w=yx3-fw@Z#YbbrixV3JS?eg}Rv6v!U0DdDGZ ze7hQ`708qt59sYuUevf0`;nD`cnGqamem3VA9MP8O%PTQsLQyjaHM2R(Y|!aO#UI) zGfDo5b~h<=E23Kz8dcv0MLMEAy=CpWNDEw9c~A$*6tKOi8Hnhs;QJ}p*?O?zl8h3>jji%3|3W@17C%xKQztSw%>6^znMwwt`U@5QZmenr4mW5bTP=U%fVbiTfJvun{W~o$>XSX>~vLB zLY~MS=%W<3yE$g9B(Lubrw&y-MIN}OjxJu4N@yVK1oyy}7r5OJll_iD>4qUXHz~9( zJ-69fY)xevLq)U4I%qyJ=B9|<(oSTvYg0DnL9MGpB!pahpWK7LRs_wq09IUJym^8y z+r;O@n=%f){ru*2H@mLIu-d)k)bW=c{r9_>M2poURK3Uf~c5?IkeT^y>w zkW-cnSKZql2WZ#K=ZxG=_G=S@{tD5-(NUL=M~(Y7U#=&2K0V*Ia{z#pDf>bvpkX2J z*I^?jz_z{Dtw58)!R?6g%bF1ZqdDx>RKHs1QJxgm8w)3!;brF4_o-XUttIxYBkQO( zaRrwGx6){jFDQqqfenMvx>_f9EC82UM}^Y5)MKK+PD9+E_DMKhXJId01>#CN&Gd`s zH!9J(UNykhgv-!Gbp8<3XmN7_Remn9daj1nOgS~(5k1{8xxcn&7kLV$bLQuFY;;os z_#Cqrahzq<89)@W;b_|_6EeSdoTB5kb`j{=8oO!C;6qlmooR z4dVkM39{21>(+@W)c4U-wFSkpYJ|CURB{@ks^fi;T)EvApGXWbOD^q@Imx*Iwm0M~ zsaC9SS+`D0!h}YPR~=Z7R&=m7gKEbUv-BhqIh5A7ssN-mghS^TE)26`o7DHeh-c?Q z=4uzDv&2LA$2T#?wjf&Br@jGVWdihLCy!hPINIxJ)82fOm=^|QOJ4UJ9hkpPV+9!h zZt47{$x9+z9`Ac!MI5||FB%OeeTuwutXrBcx>7ANi(T`Az8NIa^sU%# zCAdya5t{t%$wg-5#p9NO&|DeVL{_5;N9ZC^Mi>pFU~e<5IRbg%y54SusrC3!QxPTB zbooYtlY%D`N^l^1q1kw^_eOOtd>npv$J`cGFdvQAv|0Ct(Pb8`xK2i{MmS3>V{J2kxO{gsEE{gX}9ron>yU@yvT7~%@w7D~8& zcZ3CBrX;&rO;|OR@J%3H*pHh2(h96uc}N;=^ATCew~)ydq|aQFgqcT$l*vvM8YBs9 z($LYmK`aj?&y zNUq3Oigl4(QRWt%AoFL44h3R)XvXrDd2qVpfF^8Bp-YxXc6g3onf$x8wjnGJHeE15 zefru8MtHTa@cLrH@r8wXnM0|E@bFe={elcKGfkMYSF8MR+upfy`)zz?#V2RpkHcJp z3$93XLrT6a*5Yn=%`p1zIwPscpFLY!U&PpYWn z3g!?q!XiD_e?#d3S?hcipYp_UY2LWDD+^NyWwPI-=9p8>v$(vg(Y6#Rcno-Dr#O^Z zDn}lKl*wgvBVo519;&7&WXL^1P)ydls6j!72b*$ALRUcB@NmK2FS*M44Ej!kT`F2& zrBRxNvYGoE%c)n;I^jArIeG(-qG^q^zK3SdiZvHCyFjG%)RI2 z=O{1Kp>n;qqp; zH-?DuHG0oLujN6(=|o*G2mnAO%s-U}ME_DANaz^<=b9v23Bndb0rknEqE|fUEj{`i zfqA+dY!Z<~9A|nNX=jx*D1otvEVaOB?-7B@w{U8@WKIAea1yBu9BC)-ipFeD3zM&) zc%T89pI6YOW#l`q-%^Awr_M?+8t0|x4fQrPJnuh+A3q;2ZeJZZL$>J3Wa?nn#H^yI z6T}B^S_i6g7OvT#QFR)e^>31uNLv}8mb7gvs28uInN13RSH$0B1=1R!#+>fo1SWO= z>SYezoTmd^lUFBl#MHluWW1t?Sesv`(TO?MmP&RcdrF9?6$j{0*ppW$)Y(LKBxm{E z&&e^p?jf`Rhl_(G-XFnL;0VTaCJYxSoWxPS9d0HA*Qba8ntUdIr4TKwg9=KFI&;kw zyt!nB21>^)GS{82bsa6N6W;nZ$BS6ORjgg;G$trl!Bwr3jw~$}_>0^rCgO16P07S# znin#C)!O}8KMZ|iK)ie-#qbPSJT{r5KxZMDJAndr9KmqEzrurZs}#b6eEN(?1E5`T zuVas-Kb~Y>q3LRruaI97Ch=6fxUz_Yl~HzLh=mCq{$qL8BtbfBe$Sn9MYTeD!6k*w z2xO;h2IB6LW`9j4W*lm@nP{v?zWiLQE?rm0)J%Dn%Qs9Ljzn2fe4suz&#X;9R*?#I z+E||cBN3Lk&&tHidDFrrjO4uUWUeAHIyO-sXb6Q_RV< z-TkbXbiTMt>#~*=bJ;1!Vdz>dz8#{f#brTs&znjmapBab%9R?ZHfa9^pStoYBtQFV z-*&L)j?t#2QhcXxCmY=qvof3*aoRbIU_e>6bvQs2Pr7v&@xiMFcV063$;)e+J))`2 zi!!*wrgw~0&X`TNILL{rc9j3?1&#ZVtgDTwX6^pvtZ*KI(i*wmU{VF+?yNxCBofnGGMWU z#50VTDAb2A7kx%zY$c<5s5H+Hf_&ZBCpBSQYnYfGQ8KZpq{jrr6eGGP!%7TMf=?d~ zmHp6Bsjc;y3_A3}ObJ8f$Jof@LbBeEc?**zR^g@5c-E&Cx7u`DAI$c7NWz-1MhU~6 zqRAE7l^oKhDC1!=WjC)nqS#ZoNDHcFGf)g;?g{MOHTyIfJ&8+;x@QnJuNA58oVe=rZ2hv6ng@zH!l_18I!^}*j4_K>qnXrTz zf9g}QB5-Lkfa>Xh%^y>`V_b?)i&;*65Bh2MCRqI`==-K8^-{A&^9Mcdky8g|Ga$_8 z7B1A;i9t%~)Q?pJAY)W;dWm3Ph{GS^)t`#jH5!SfX*zLW6Jm2K7P~2K#Pc7p>kkZx zYt_&pudw7sXJ$yW4@{+d4H5Dl%PPgO;NTND!yZc9o#A3HuI&yy@+<5$|o*ep!6TY`|d#n)JSL9-jNv)6s=#Q}4 z<>N0JsN~`Kcu!HQonAJ2wgyiOrBGm!tKXw9A5v-k2~LFLa}C7DP{077(tv+4$*7Mt53v`Sbas06)Y5VwR zlXo}ykd@_JCeohX!Ym2P>%tpmiY{mm*h-X_p#IV!$c-O}=+VfCF3;8sD)+G(;E_SZ z_6kRc%J-!4(Gyh^!N{!Du-IFNm;j79le;7?7?ocz?=L{y92;l^IflLKp%<3N71 z|B0}`l3k+y76DnKyTcTrIoE<18hXfh&>%f60|bie39PDK-A_8Q6E}+PogKO%;u*}~ zuD-O2@KX;$4s^1Yy<-?7{pemwx#-EkCVs-S+X%JEJkq=Ek21A5!FQH8Z#mT4!l6(v zm4HWMWFSarblwpbX> zKOxy}qslz7y1I|%Uz3Y*j-y*~(p@LK+E3{KI# zr4RIGZHAxI$7_(a+({Daz^k$=nX9xvrc@Vv4-2T@QP*LAyl(8R_Ml^p7cq_8rQU1- zOpRl-b`3F;gevoFt#nK$Y2xTAT$TMa%-3R#DCPbuOKx3#yLnB&>5&~Tns$VEZ8n7? z6Z1M2qHU<6<
    c@jJLlJ-IMPZ>=O zMz@L!f%BHwTwDS3r?8}aSqE*4j$R3lz}F{@_fBg~MNe*yh%hS*qJ7|g)S-k$dVz*< zhpnpDSauV~Y(Z5f zc9;{AB0FA>`Tkyx8d;w;vAw*71c3jia+K;{%F&#c_ z2ujo{9UT$j0}DvNeg=pq0({1ew`oOZGa6swwzP!@#1Yf5%e zEHFn_9FFZ)WN@fjTv%A6VLolLpZR#z#1y^Zg}`Q-dc5Fv#JTPI@!0KZ(Pnp#92p>H z1ruiLD;;Jqtf&xW+pcl|6-;NS#YC?#|B?WZE})gC1Yj~y4X7Dnosf2NOB3KckUi)E zaoKq2aQ%rBOjr7N=)HkaJbFX+@_N@>ivv5oFTyb3>;xx3o{xYq4JQF0(I9J{;|+qUv9 zw2&O9yisq0D6Uf=hWmlL`5y~ut<}?-x7xsvCBIqr`645vr%(Fw3TA!d3l|K{gV0j4 zoc4cora*xvb)4$D6iydd)|Nh*DxGH9^~H2HGS{)8cn?`jsU#fQbs;RCk;OS7gA#~* z_tlq@vU5C041)aY=*paQE?iJ7g5rKg%M|e9cPbRx3YYlp1ATl1Y2kfHU_eaZ+VgIF zILUNiA#$$_Z8PXtYwLKjEP4O8@~EoAglOxjhk{uGpW;RG;qXl&JROSR3MB_>VWg9y z?>*pbCK)D&KA9KEpe$gFKcb^uP`NZ@*eMiKQZ{#Ob$#0tsFoPaR68s*rJ%|zc`WIh zo|_rVq3(%8ClmNEI6+Rh{&^H`9P#WKghh*e3Nc*aPC}BZai>je;Vb$3EA&yL^QoaL zOMhO|A*ks*h)c>-QhPb!@G+(>GvBk6J0o^Q6v)ny9<NPfx8N=GypEQ>wfF3rNN@lbjRNy4u&(7@78M#YwHu{UslBqi83mXO37Khr^Q{I z-ZzKhig*)WI^Aj946LO`i5=zEEP&=tlKddN!r(a#m`P^)MDVQ-Y#__ z2gTK%j20Jckfh&gf5T7&Yn9zX<~a$-s*2ckxj2^NNP=`gZ&G^`O0~}!Vx_rS;8=#Q z&5uBvq^3suRtG-`6}+4F>uE`eB|#jj+DCoh&gn|}MqhF?_ptu96J#`3>moJ_+AIB` zd9*3*Vn0G_KLg%NKfzsW4Dj~5fcv>=boXyNib69C-FkLSQM^kMTKBrXYf`EBz|h<{Iduj_G zQ=j8*ZfK_ubl|~%OiD&XR$H{S8E8YDipXXh?8u*z4iqTsi85=VEhJ|^q@#J7sf+@xxhYUIhSNWk zy;+MsksY%nx{Gv}v91Mc(KouBO=X|$o1=wPIwn+xU3c{uRYN52z6QrF^S904+7lO7 z`d`fsf92|%xKk-ffL0onKJSh$5l(Q4H;E-P;&y0R-(1uy`Xy3c9@Qhy(p#{avkj|+3uM}vKgNtcf z^&{GsyfMTXh{s7$_!k0PJE#$@uw3EE%3>A2gV@aok{_o_9eovWh&rW;wnLLWqvR_Q z9nmxxr?MOwsvw29Tm?h(PNf%2o;HK&(!&nD#<6}$XB@f~-FcWFl8c*-O9|&S#ZXtO zaiP^9o0_MgM@&I>tNG}Ub({}Do303&t`M5+ZPTYOItItg1cfk|OuxIi)}l_tH7<*j zTu`eK&)d_ec}-GxL!lql>1e+ESUtHB?j{w|c=qGy=RzIUgAVJ}f_PeFZH07*>SpOw zzrbrhB@{d~F49{>YE$XzWHHmpukntZvp_O&QAy<(SUZ38eWYrVNFqJ9U^;=f!)IrMH=8Uqe0LWOhFTUCGf+q;jNCBW8A7 z;ns46d^`h;<&fgEfZSLcM7@L%=1fdKGkd{|b-px3d~jtL5Md0iMuFRpz^Du%PVXB# zH8zz(7?*UJlk;8L5Ue(tH;qu)mPnbmh7@wYG;YCL#QYX$`!sPJ3`Apv_)QUWv}3b8 zQlz(4V)-)>y3KLTC%uq_As|MXSeza%@glzO7yIn7kia2JNI#tT}KyGh|cHq&mTh zR|eD#4V5zQ+_m8cJwA(l|L6uQf2LgYdLin#VJ9f3#e@`M8f)lVS1M+66LHi$8OLJ5 zQSQ(+Q-&Pq36gq6y*cjCv6o+9CP>iJN4-(aITCugzid(-3;GUdPlwKK(`@Uu4YNh? zKy2{JIiZvg>BaPQzf<@eSO6<04<{;5(>EbMpg@=>lT9(1Te(8Tmz?xQW3U5FAuOPv z#gGAgegb2mbW69ipo2%j7ry{ast^rBu9`U?DP4_{KfIt_z>Zi`F4$6qlJRjvaIS;m zb`*R6#%G0&vRzYyZC4~ovSP_b@O7Hf+tM5aF? zBkuh0j(=`QRGw@x&kBLjgh4iDC>JWnjrArGq|sHCB({f|iR-pH?+eq__ty)-U{w)1 zq8G3h{rmr)3QWq*_HXc0%QEwWgAXK!e4qLP7(;=}OAvUxN{}F8j+Ey0buslEYMv)! zM+CUiu@O^Ma69->9k&l=w;Q)Hw(hsjA-LfYA%L%{5vpUVFcO&Qt@PItT8$t`<^5L| z>@^o1;_pi^&YQt~Flx6Fg~7hC;mH^G6Z=gpUd-zCu<$xJ8PQ&Nd9q!QMjr*2+bSSP zFU*@w*=G%V2ZZx-qR?BQ)i$F0ZBUx@1g~Qam+J#i5$v7ZVl|=4KCQmnNHzdS`rd z0`luiB1P?cuDMCZ&Yj8ZHlW^Jm9rhM5^l*Xr6bq{Ff4Xwczd57q2oV+2k;Kf$B;x+ zn~7>5YOjsVfL>=}kB%U2pLW7>Xj}2L*ML*X6?f~r@MeNmi=df5k(YgT=>_Ko0!nf7 z4oc$%KsE7?04nPLhtipV=J(>cI#%ryx&VsbveiM+A#13OQBn;CphljYC?4mp^P-Pi^Qozk-=EJ58vsNd$wO6ABv;?135)DQUW&Z^Na~~;Mgl94$sZF4E@}Z_QO5dQSY``?DxsZ;n z94nKv(sfF@!J(72LDp>bL2b6;##tlyu3;|n%+R;~ zBc5FI6_&T?sOlYtz%XkWkb6e@WxnRV>ljhj6dqj5JM=DBt>5+?536x@-k~ynR72F`97y>fVz08qNHg>QK0)$MrXoqh=FkB(rHhvsF z68_Mo&~mT~kmzIHm0mM8#3P{1EGkPrOi!=Etnm>`O+-g~LZs`vfW;Qr8>-X~8AtA^ z&E7NS?tabO?9G>?YsmPRND@X2{QlKM0#L=Iqghi`M)v8~xOd#wkZ$SEpd8tc)Evcb zG48@HacQHRg4m;+l3Yb@UYrGPQE8LzKAbsjL7XLzByPO-^lq~EGSqW+dBTe2UJAVoX8kl$J*3OA>xmKLPEZ;8$j7U0y)Y-ZoKX)bUsn7! zBwYR2qQ0!7yOO_L*S3U5ajkxQz`G@PZ$FOmAj!iekXJXD^x4Qtk|8FPV8|7XGN>*x zi7GTv6LFiAZ3w#5bChQsq-Fve>gV7)+8!`?OSJd=x$F7OY-YH~VnWe0X)m*No84_# ze>HrSnd}pqwWIs(jMl4PisHZbc>j6vJ12ftK+uH*}3j&v{Jd9;-$kz^} z$O{6$8E*6%d*8hgHSoaRRMb(yF9@8!HunB;pfPG9v#MibLf4G|k^2&d;f^KHY4`3) zL?yqMFa$EwXb)F(76larHQ{qY;+uCUsLG!S;NOzJ*bf3q@12ur^D?~Xm(Sk=QgHul zfSjGJ$bW7BJuqp6(tx*d!wNiiBqYoj9RfvlQBugwg1*7kZgJO85&=c;J#uD-fLY1t z2qh8CLA^O1PVPRp2Ptc#=SRRJ;#V!uE1{Z#t~8^l!!#+y*Y#Gr%P z8i~2w8C-a%py{)B0a_C2_HoUObIyENim1qM#qJ}1ofW<}7KctG(p;JO=ip}5;_XshiXC4fNA!J&PXQFB;_=` zuVyE2)24@(I>Qqnlfc8PnIm|Uu~}AJb(R8uhn=OJ8YI1~4j3sJveEV}q!*hS;@r!Z zvFL!OiwwDxVzW#8XyA~9+^i^$)y~2Lu5xG~OB@H%BjgxA(O-N$314_}6K0t?OB7elZg4CGY+}?d3n$NB zwcxei;RkWNJpNDgr|ySW4d4KO9sFKf5Ps0X%j0hi34br}+LG{tpkCJJMc}svg};}1 zZBh6^H2;(NtzqHs#a>$$evtCdV*hJk__ZQNCY-sr7EdPv}e{E^_K`sBH z=}+n4*9H6;2Kx%T|3MBftMU76zRb*jO#FF}KVQH80>c0GOMXTtz9MRW(3=i)T|c|BG9pt_d{|0mr)kNdx8j92Y{ z=lp++JJJ;Yt(5*=; s0; + for line in lines: + if line.find('->') != -1: + if line.find('__start') != -1: + start_state=line[line.find('->')+2:].strip(" ;\t\n") + break + + + # get transitions + # line in dot: s5 -> s5 [label="ARTREG 20013226 / 531"]; + transitions=[] + for line in lines: + if line.find('__start') != -1: + continue + if line.find('->') != -1: + transitions.append(line) + + # throw away transitions with the keywords : quiescence or inconsistency or undefined + #transitions = [ t for t in transitions if ( 'quiescence' not in t ) and ( 'inconsistency' not in t ) and ( 'undefined' not in t )] + + trans_out=[] + regexpr_transition=re.compile(r'\s*(\w*)\s*-\>\s*(\w*)\s*\[label=\"(.*)\"\]') + regexpr_tag=re.compile(r'<[^>]+>') + for transition in transitions: + match=regexpr_transition.match(transition) + if match: + match=match.groups() + label=regexpr_tag.sub('',match[2]) + trans_out.append({ + 'source' : match[0], + 'target' : match[1], + 'label': label + }) + + states=set() + for t in trans_out: + states.add(t['source']) + states.add(t['target']) + + + return [start_state,states,trans_out] + + +def parse_labels_of_mealy_lts(transitions): + """Parse labels of labeled transition system + """ + trans_out=[] + for t in transitions: + label=t['label'] + [inputstr,outputstr]=label.split('/') + trans_out.append({ + 'source' : t['source'], + 'target' : t['target'], + 'input': inputstr, + 'output': outputstr, + }) + return trans_out + +def split_io_transitions_in_separate_input_and_output_transition(io_transitions,nr_states): + """Split transitions with both an input and output event into two transitions + + Makes two sequential transitions with a dummy state in between: + - dummy state is labeled : + m_ + - first transition : + -> for + - second transition : + -> for + """ + trans_out=[] + id=nr_states + for t in io_transitions: + midstate= 'm' + str(id) + trans_out.append({ + 'source': t['source'], + 'target': midstate, + 'label' : "?" + t['input'].strip(), + }) + trans_out.append({ + 'source': midstate, + 'target': t['target'], + 'label' : "!" + t['output'].strip(), + }) + id=id+1 + + states=set() + for t in trans_out: + states.add(t['source']) + states.add(t['target']) + + return [states,trans_out] + + +def transitions2aut(transitions,first_state,nr_of_states): + nr_of_transitions=len(transitions) + strings=[ "des(" + first_state[1:] + "," + str(nr_of_transitions) + "," + str(nr_of_states) +")"] + for t in transitions: + #aut_edge ::= "(" start_state "," label "," end_state ")" + strings.append("("+t['source'][1:] + "," + '"' + t['label'] + '"' + "," + t['target'][1:] + ")" ) + + return "\n".join(strings) + + +def dot2aut(dot_filename_in): + """ + from mealy machine in a .dot file written by DotUtil.write of learnlib + we create an .aut file containing an lts where input and output each + have its own labeled transition. An input transition has a + label starting with '?' and an output transition has a label + starting with '!' + + """ + + if dot_filename_in[-4:].lower() != '.dot': + print "Problem: file '"+ dot_filename_in + "' is not a dot file!!" + print "Exit!" + sys.exit(1) + + + [start_state,states,transitions]=get_lts_from_dotfile(dot_filename_in) + + + + io_transitions=parse_labels_of_mealy_lts(transitions) # each transition has input and output + [states,transitions]=split_io_transitions_in_separate_input_and_output_transition(io_transitions,len(states)) # each transition only has label again + + #pprint.pprint(start_state) + #pprint.pprint(states) + #pprint.pprint(transitions) + + result=transitions2aut(transitions,start_state,len(states)) + + aut_filename=dot_filename_in[:-4] + ".aut" + + f=open(aut_filename ,'w') + f.write(result) + f.close() + + print "written file : " + aut_filename + + +if __name__ == "__main__": + dot2aut(*sys.argv[1:]) + -- 2.20.1