From 363446821e8896b22be6d8ce0400f7dbb61de0e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcin=20Pi=C4=85tkowski?= Date: Wed, 4 Jun 2025 20:21:51 +0200 Subject: [PATCH] Released version of GUI (#5) * The most recent version of ReactICS GUI. * Small fixes + folder structure update + help file included. * Added export to XML (for data sharing with GUI) * Released GUI version. * Automatic update of the reactants set panel + help content. --- reactics-bdd/export.cc | 103 +++ reactics-bdd/export.hh | 2 + reactics-bdd/reactics.cc | 17 +- .../help/img/ctx-automaton-edge-details.png | Bin 0 -> 7886 bytes .../help/img/ctx-automaton-panel.png | Bin 0 -> 3741 bytes .../help/img/ctx-automaton-state.png | Bin 0 -> 5242 bytes .../img/ctx-automaton-transition-edit.png | Bin 0 -> 12138 bytes reactics-gui/resources/help/index.html | 321 +++++++ reactics-gui/src/META-INF/MANIFEST.MF | 3 + .../reactics/ContextAutomatonEditor.java | 693 +++++++++++++++ .../reactics/ContextAutomatonGraph.java | 438 ++++++++++ .../reactics/CumulatedReactionsViewer.java | 13 + .../mat/martinp/reactics/FormulaEditor.java | 410 +++++++++ .../umk/mat/martinp/reactics/HelpWindow.java | 125 +++ .../mat/martinp/reactics/ProcessEditor.java | 427 ++++++++++ .../martinp/reactics/ReactantSetPanel.java | 49 ++ .../umk/mat/martinp/reactics/ReacticsGUI.java | 791 ++++++++++++++++++ .../mat/martinp/reactics/ReacticsRuntime.java | 198 +++++ .../reactics/ReactionSystemEditor.java | 409 +++++++++ .../martinp/reactics/TransitionEditor.java | 208 +++++ .../reactics/TransitionSystemViewer.java | 367 ++++++++ 21 files changed, 4571 insertions(+), 3 deletions(-) create mode 100644 reactics-gui/resources/help/img/ctx-automaton-edge-details.png create mode 100644 reactics-gui/resources/help/img/ctx-automaton-panel.png create mode 100644 reactics-gui/resources/help/img/ctx-automaton-state.png create mode 100644 reactics-gui/resources/help/img/ctx-automaton-transition-edit.png create mode 100644 reactics-gui/resources/help/index.html create mode 100644 reactics-gui/src/META-INF/MANIFEST.MF create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java create mode 100644 reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java diff --git a/reactics-bdd/export.cc b/reactics-bdd/export.cc index 6682cec..b8fa322 100644 --- a/reactics-bdd/export.cc +++ b/reactics-bdd/export.cc @@ -808,3 +808,106 @@ string RSExporter::formulaToStr(const FormRSCTLK * form) { return "??"; } } + + +void RSExporter::exportToXML() { + output << "\n" + << indent << "\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + output << indent << indent << "processes_ids[proc] << "\">\n"; + + for (const auto & reaction : rs->proc_reactions[proc]) { + output << indent << indent << indent << "\n"; + + for (const Entity & e : reaction.rctt) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + for (const Entity & e : reaction.inhib) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + for (const Entity & e : reaction.prod) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + output << indent << indent << indent << "\n"; + } + + output << indent << indent << "\n"; + } + + output << indent << "\n"; + + output << indent << "\n"; + + for (unsigned stId=0; stIdctx_aut->states_ids.size(); ++stId) { + if (rs->ctx_aut->states_ids[stId] == "T") + continue; + + output << indent << indent << "ctx_aut->states_ids[stId] << "\" x=\"0\" y=\"0\""; + + if (rs->ctx_aut->init_state_defined && stId == rs->ctx_aut->init_state_id) + output << " initial=\"true\""; + + output << "/>\n"; + } + + vector>> edges(rs->ctx_aut->states_ids.size()); + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + if (rs->ctx_aut->states_ids[trans.src_state] == "T" || rs->ctx_aut->states_ids[trans.dst_state] == "T") + continue; + + edges[trans.src_state][trans.dst_state].push_back(trans); + } + + for (unsigned src=0; srcctx_aut->getStateName(src) + << "\" to=\"" << rs->ctx_aut->getStateName(dst.first) << "\">\n"; + + for (const CtxAutTransition &trans : dst.second) { + output << indent << indent << indent << "procEntitiesToStr(trans.ctx) << "\""; + + if (trans.state_constr) + output << " guard=\"" << trans.state_constr->toStr() << "\""; + + output << "/>\n"; + } + + + output << indent << indent << "\n"; + } + } + + output << indent << "\n"; + + output << indent << "\n"; + + for (const auto & prop : drv->properties) { + string fStr = ""; + + for (const char ch : prop.second->toStr()) { + if (ch == '<') + fStr += "<"; + else if (ch =='>') + fStr += ">"; + else + fStr += ch; + } + + output << indent << indent << indent << "" + << fStr << "\n"; + + } + + output << indent << "\n"; + + output << "" << endl; +} diff --git a/reactics-bdd/export.hh b/reactics-bdd/export.hh index b8b0714..bc7d3a7 100644 --- a/reactics-bdd/export.hh +++ b/reactics-bdd/export.hh @@ -14,6 +14,8 @@ public: RSExporter(RctSys *rs, rsin_driver *drv, std::ostream & outStream = std::cout); void exportToISPL(); + void exportToXML(); + private: RctSys *rs; rsin_driver *drv; diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc index c86fec5..90e1298 100644 --- a/reactics-bdd/reactics.cc +++ b/reactics-bdd/reactics.cc @@ -17,6 +17,7 @@ int main(int argc, char **argv) bool reach_states = false; bool reach_states_succ = false; bool export_to_ispl = false; + bool export_to_xml = false; bool bmc = true; bool benchmarking = false; bool dump_help_message = false; @@ -32,7 +33,7 @@ int main(int argc, char **argv) int c; int option_index = 0; - while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheEG", long_options, + while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheyEG", long_options, &option_index)) != -1) { switch (c) { case 0: @@ -57,6 +58,10 @@ int main(int argc, char **argv) export_to_ispl = true; break; + case 'y': + export_to_xml = true; + break; + //case 'b': // printf("-b with %s\n", optarg); // break; @@ -141,7 +146,7 @@ int main(int argc, char **argv) } if (!(reach_states || reach_states_succ || rstl_model_checking - || show_reactions || print_parsed_sys || export_to_ispl)) { + || show_reactions || print_parsed_sys || export_to_ispl || export_to_xml)) { FERROR("No task specified: -c, -P, -r, -s, or -e needs to be used"); } @@ -176,7 +181,7 @@ int main(int argc, char **argv) rs.printSystem(); } - if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl) { + if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl || export_to_xml) { SymRS srs(&rs, opts); ModelChecker mc(&srs, opts); @@ -194,6 +199,11 @@ int main(int argc, char **argv) exp.exportToISPL(); } + if (export_to_xml) { + RSExporter exp(&rs, &driver); + exp.exportToXML(); + } + if (rstl_model_checking) { if (bmc) { cout << "Using BDD-based Bounded Model Checking" << endl; @@ -269,6 +279,7 @@ void print_help(std::string path_str) << " -v -- verbose (use more than once to increase verbosity)" << endl << " -p -- show progress (where possible)" << endl << " -X -- backend mode (makes output parsing easier)" << endl + << " -y -- export to XML (for GUI tool)" << endl << endl << " Optimisations:" << endl << " -E -- disable auto-reordering optimisation of BDDs" << endl diff --git a/reactics-gui/resources/help/img/ctx-automaton-edge-details.png b/reactics-gui/resources/help/img/ctx-automaton-edge-details.png new file mode 100644 index 0000000000000000000000000000000000000000..858df8edb0b298a34fba4b26bdca58115c2306e7 GIT binary patch literal 7886 zcmeHMXH-;KkbZz7QBsQuqzOvSIp-|U0!l_{V$)=r90i&jB^XDK>HGS1)vZ_c)va(}hr!epi3#oy002O&tR$xiUN^u` zIvzGSZzau&fR}JjZC#Y6i5t|x$=(8CV-7`mIG97t-4PZ5;6Cva(eF-p}%99b+0(bYbl zq{dx&B5Tbh;dkZBCmdYr;eB^3MciTylu5T<-4=KnCRkE`p>rbEe+HZa*V5TtUD{ds z0e}D(0cxeI_E5ys-j>6}%pPve;cn{ystW*OlI{*Brbu%X6mD*buoI`-Zf>K4BFx0; zbokY{)Es2Ztq@9{PUc#k>e{BBNK;`mI!OrvF?SJAfUP;o1nO>UW9Ka5E>8D{ToLg5 z<>vlbvxgnZ#GT#Fnf_A5pEBgkolTt(4k(1Z z9rRMB3EbWVB~C{N(xJbFUwYs#>2}V)K>*?4yrgh)b8vC~S9TP_;(uVjr2Nf(xmW~- za5uNnl|$H?+c|?Oh|}@#3j87LZ>rvZp>p%{|3ST!B%*9I4_ap{0$}O8P304bBWLY{rLAG{|MuM;rbV@e}uq4V*Yn` z{R`JWLf{`U|GT^Xf5AoYcXMZM2X=IBVC%-N_3J6v_Tf0oC~M>4;Z1(mm<0feX=OQS zZTE@IOb;oFv4am9O5@2vFVIplq>pk(uGSosj%p@0sXnT*HhMiLV`P0cdcNVztYI*N zv}LV*Wl(G9B7Mc|ku(|XX_fv>w$7_$%Gmg%MEECZZzUB>iAZJrrG9vyr#%dA6g>2H z-fA>i5@kqKxrzt>nDU(z$^^e6O-7Fwe#@gXca{`dgoZIe!sO^;OLB7j$EC>Vr>>)A zXk(Qa$irYvY;0_hh)#@Zl`b189v21u6n3dLOQMRZipmviX#@hHtPHNCjVse-tEi~x za>8DPgUe)cnOH7IoJt`$WO83OG^C984-5#-W(WufP+brCFyGkR?A&OWg`2RqhoX#F zoSl8Q=;XLZHZ?Lb0=aoJIWdtLLXZn9fiao!q$)9JGC@E=Xf&DtomWtRncdwz^1dE2 zKR5UOyMqwbb=oKJbcOud109CGn|ybo6!JlB@7}%3k&Lvn>tEhwXJ;3tiq6c;jQ?Y_ zw6s)LS0^UkP^kF;)72gS{23anw6?Z}fjb%*Wx|-sD=IjcnPYp*78e&W{gms20@C?| zw}^0)dlwyq9zKZgG5hH*CXn7|#)H3k$5lVBof^({%hlCYn`LxxaImW@xD)<}2|||% z>PQ~8FgFLcv$M0c?X##J{g4kANel=G=<4cv`I4nnTct$n>`hfwRZfmnsWt&x27oT1 zK%=!;L<Wu${NP303{{GQH-SL-ov2sg>#JXQXekuxc3pVk(Z)N zyV~2Is~5Xz4~r;BF_81~^RHG9caw%Q5Xd__JL~A^z=2Uu^D5ow=xA_zb$r*=*LU4D zlv*n(8xLJoW}_S%8&fSDT3fSrNuyP%I6n5Q(j@{gZ=}QzO^Bay$+2Gpf=0^A%QG@F zvHW#wNbg()1k!EI&E>saHa9kI5h;+|y{4J`G`y5jkUQkd$Os^1YisN1She&f|0t*| z5gUm_Mudmgs84?_e1s%jRYMl1rlx`z9vA96>)%LNGBmNUD9SQvFyuhXU;*&OsG09} z409EEnZr%sZfeq1gkkW8IDW7QT#=9b9bSJ0nKVcXzjZkW&?%5YxPQ+%p=6k66Bb$I zP4}roh`1k|2pqe;4#k4Ht30LB!wAXUUw9_`{Fz!LRJ`)Rmj%geZ~u-E6z+N*4SyWS z#m-KwNVVz^$J?nuzSFd+I5}}E;F1}9>R%dk!F^Un_H(t=^2&-1XH&m5r;ZH|g#Emy z{Wu|>8DikYGMOl8zZiV*fe2`wxH&`nefx#hnakPFDAt>p_ivjftO-?FL9U37^k%rY zZ~H?7jHUWUuTmHd4-XWz`Q#-<_1ldw-5)ES$Bp+WZzQVRsNFsh9pi{{KWstJvTjmY z{bbbqo_{hn)SqXjW`L=$EV3xTc#+(>Q}gV8RY*Uoh&S^o4bPlMR)1?|+AU^EF>F|4 z!~Q*S^Q7XKN{fIDiaL&YxQyd-K#8HX_;BHC1ods3{kNrwa#u;ViymZVViSH zk{%Xq=dxhzyo*k6D{lBH-XY+vNEZu+V?TR#DB2@%=8o5H8#8C$hk0)!Ea;JI+4Yk# z&ihl1u84P^A5mEPDs7kuHS=T`ohd{P#%|Xhochvk*(~^yhnX!)?cNbWz5hhQ{;GU5 zq)-1?PeH}|k+iRm5&I5fs?IP+S9S@kJB4cNN0k-~lZhQ0q7a=uZCx1abMj11Xdr)P zja?Ea4AN*h*&h1i#priyY8)wj_`)8EWD&3MZRQ>3;+QX^PeLlDjz?R6Ev31iLf6N( z1snGd^mjT*zSOyfeee@L?O3`U@#N(CUGc?0b9BHr8R@Mk*5#R7{9B&K!c|-`9qau2 zf#$<9PiosT8ax)Ufk-@eW#x&v4yuunQEk7sN0uV-KFbq}DS@KhkdFz%s-xS+%Hj9~ zdhM<*jQ0Y6u54wNoJ}5OO-Fq3#RnJpB_Ma{%hOms49^h@sXJ;8)A6j_gO()m72Q!9C#+ zAjLrU6TX2Z!q!=0sXHFNgC3tLFSoS}d6l1Hfa+#skHy3CZ+9Klw?MGhp(5P(M!vG$ zyw~~dz1uG-$1uA~hc1l5nSu>Ms~foez}dqHrUIf2Ri=mJaBQ zMVzOwq}aMg#kxBC0>@v!etpFs%*J2(pQL0H0;2DAthW-B?_+`~Ce0@T5yF#-4B&ipl#zp=sVT=wP zt|Gnk0&>f&xhX$X^lBYz+pME{m@ejU@5}Np%dj;xO1=m-V!!Sj=VvDgM{3yaus1$b zFzLL;>r)m`GI%rI0`I9ziNU+RGt z5r_8c46Y2n$SgcSCoa!G^j+sGK>%_?%s0vC9*#d@o0|dTg37M46?l;yKjoA~xsVkj zY@^{qWN?v*6Xi>LAV}xDp6~D2T7j9U;152Ix#nMkiT`}u!PE^2S1GhEsiZenk@M(d zENr*G3S(N*tXe6gnMv){SvKwCmLqfHYV82?Chwy0(*C%tqy#giAiqFTV$!!3m;JGA z0f|@G#h>V6m6RV{TjVK~d6EWkc_Bv^m37)G!B}4`g6*&UQ*0Vb+PMevv9Sav?`=l# zu?XT(dvWe)#xGe_XfL-7V z>j{!51WEe-aPu*;HI;2)+D3c1xZgVip!D~1TPx~HppskN>aPs118(+DU%iB7M2P$t zqC8{7#gWn+!D@WSlB^t`cO5P~sP{0dWgPkL1u{9#_h@PNK(nxG&AhA+GIa8kRkSV{;5kXKc7ha z_Nusx-7Nq^{q?9o?)~=eM2^We@a~=9OlwwF!UdP;dA(74E;23qBY?de>_O~4KhUep zc;KyN^jJDK#XxVeVgJBsN&M9>OYa7eonM?fai*Nv5f+U$Rc6}TxP28F%w8qn4rtSe?j+bMszD^HeB zmiQunV5;AJ^9uYYSZKha1I}P&xGXvt>0L;{)o%1bpB@&ABGf`hJ%*=i(`%OWg;l!c~J*;T1iJ#fy zA!xOQ^z9%L>N#4Gm8NAq`SmLmrX;W(=9A*HzL%RF97(hiE4^w=CqU#Atov)_e3f3* zl1;zw&|B?=*Wt)Ho>v;hKz?5`k4{oAxVChAl|QOy@KbqAj6FK9ycoCeZdgi+|Hv?@ z$rNeLGkNRNFsGw8cC$dGa7fbu*4HI)9bXTZvzgTyT_dk zrkY{h?Snn`n3Q_PelA{m3O}da!-PFdJb@l_RQsK~LdEx~<6XX$=X7`#ie8Z~>l7fC zUzoNhPElamJlYb-Zrn0#u36ZvM4%o3R5Sbgpvr+aUm>im-;#PU2p>Cq4!EJus2nZ9 zXWp*~hJG#oC>Vg`(VHHAJ;j)038+=pF<0etSzZoITaD-N+CwmAZl{*JL`t;KHF&LC zd(QQM#iY6Ekol9JyR~1C_~;;V7RHikVvE!JRm_=^@b@|Q&JdR^H2OP8cOW^+Fj6Unj~HSvx>vY1(^aVWzv&)3$%jG z=?da@&I^iq1M+b#YSxdvd)dE$oYGS6-53;O5?GsjJmnqk3%mZzxPQ+W2YAc? zKiOZs@myO|Dw0#0v+|t#njb@*xDT$8s;DR(^oQ|MZM%I`Ur&>C=w-#jV8KnMw_atx z=SAZ6y)0^gtxSJdK0@%PeKxb1&7kmV4HMtf+U0z8Z<^JJ3erb8DGBMK+;K*d`)jqG z&n^wx|J=Cms-5Srj&c~=_wFH&CZ}x+sYR1oVR}9J0V|!Ez-_)8tNx5)1e;Eb(6M%kdnJMCJ-aqjC zF-BY~I3FnL*W}>|ssPnu@}=*}2>WK~P?=o_E;fvC*ne!q*Es;caB5 ze4{x7?<>jz@&XS?I(uEl?~x6!d{R8*F)&c%9p~^fR<|puWQ8nb`3_FZ7ZTBk-Ul-% z0hH9t3yh;_3A1V({5L@UM)b#H79LQ84F%z5{nxT(621D(PY& zbu9x6@bU4E*P!-hnL7_0$U3c!3076L-+oTxz2{;5ekUluxyLNLta({YUW(QEqeYCQZ=J(Uzw zQPLMbX!c0_hSzv^o^oK62t}`~>Jl}h@Z}?)J^15vg!=madY{${b?iPZ()erOR33I& zx&HH1HP?^Zr-dTHODn$h7?XM2v%7Us>$N`ND&Qz_{5gRn=?tk;gO4`b%^E+XEN{5w zRs$9eMl-lL=T9XyA#S_lQ`b8567v)n6ScY^zXq27=URiwi=EG6oxh}|cN2;wsDss# zt+Ix|>;)#+G~k_MU|zmFpT_e@!kyaD#I*X`>-cHKC=(cHzwm{)-|_S&k~TZ2OqEG$ zH^B~skG*whi5Wa4p8L!nqLBjW2D)`F)Wjf2-*Q%FNBK28P>20ArIxZ!LJaiv?tT*o z@w5Pi$)}q(pKBRt)tZmm>}N%ZMjO<&QhnJ;X9XW-3(^Z)KwS`Ezr*go#9WCDdTvu{ z7n0AhL0Vu6I`azeAI%X4L+J{-0Ywf@DPorn`SUcrx<%Mr5=2GCUtlm;N9a#_r5FGA r%dT(q_&jS7f3nkF* literal 0 HcmV?d00001 diff --git a/reactics-gui/resources/help/img/ctx-automaton-panel.png b/reactics-gui/resources/help/img/ctx-automaton-panel.png new file mode 100644 index 0000000000000000000000000000000000000000..2fdd1f8ab1fceb30a2f6e0b6810de4cece4d2761 GIT binary patch literal 3741 zcmY+H2Q=Kx*T;WELWJm@>_(U9y(D^Fv1;_*t+E7BR|tYdBubPhK?qjwEm1e3TfGw^ zM1P3R`mg7G&wKvwJ!fX_%-lIM^F4F!oKK7nRE?CFkr)5~QVn%wJpjOm;(S&jd|b_$ z*inLOZh0$e7!VN=&HdC~#&x-URE&L;UO3qJxWGNY1}^RnfS(VX7c49YcDI4y8euVB zu%M*0kf^kX$Q+diB>>!isG+Q2;GemZ6{JHo^`Pff1d%h*-COCf3|V!tVX1_Aj!_Nu9Sb({QU$*vCL4D#_5cz!W2>8mWRGs+ z3zcF(nJL?y)6thPMue8A@P> zVc8t$n$5TcoUby|cGp+?wkv@xZ`XI16)ZkHo9;~=_tnuM2a=PMNt!;PMHoopAa96# zZIx2$cXg(mc0=twGrJ^WlvxpL_4W1e`=DmT#Y;6cnS>sur;Y5cPUW>6Usw=>jTgm6rnhp zNWcwI&mR#IM#Us?vS6Kv(>CbL1pQ~JK6*+rhso~`$vpT67` zxGEPNraWwAq8-nujH=3LXi^pyEP#=T2@X_ICWzd*_O6g^wpw^vnbL=6CTpYxdM3|x zvqQFvo*9OS^67I^Dd|S z?~lC{DFJ)O&vNem)v~+!%jk#G*|H%bh)YLG-!#XOPZTf{{Z)H220i4Su!yN?^7W}G zX6hON_E|3HGVm&^vt{Hqma!Ef*Ev>&YsCt&x8Z!9At zV}5>KQBkq8v$M3+^4Vo^QPGdVLB!>0l{`2ai6kbuw9|pZU=Ve69d2sZsd9_2fnvH; zEkW%(JUkd!or;QzUU6+z6=q^WjF*>}ot%s1B7iUJ$k+veYbrGRL(Eg>PHbQWdJ+KZ;u@9}f30X0!kguY&) zj9P(#=MyNSxw*L`O~~Zl)x}8yNDjM!VY?qC;?S48zwZf$!;!(K!6DYx%jZX1P3HW* zvi5!cXl__EpMJD{a`am^gpXDI$q`xFU!hsNNG$gQGGMYtdFL8-f{wjC2q{qTvi)38 zR`&atk3aQeqx+Y-x}zPCM}3LGxYod-N>Aa8wCbveQ!Mc5{9Mef?mUnN7)TSFV%OrN z9~V*_lhtx1k(-p8FS!EQHDo3e{!ClhW7StsJRH!Ni0T8Tv^; zNT^w$w=Ep_&kDLLicC9AP=S|rI9+7@$9uL^ehcAgNSWc6!a~bNPn(5i-^j>FE@&pu zIjE+g5i=AYEf3y5JVaI87-8tc}e8nC`6ARtg@Pt43@ z&Of7nURac?>xHDm_$e#DDjLi9n>$9B9&*VQ10CWY&MwxBjs2#vNcR zKpF?}#ug~;DZC@00iI&Tm)#~9k#|?sL-#g%vLi_7ZngcsgGvoPz)YaXy8p@S48f{uU(DwrCutove_qKg zoaN?~`g9QH7CO38-?L<(CcX_wN=vU?+fo3|9v*i>G5KmtZfhGG^yK97x!b>fMF>cU zi{s1t_=rAmadsYo>zSE-Oi6ieWwo@pC@Uxk0FZ*wqT5zhR$N?Ps;jGuii%|Xb|s~x z&Q4E9_Ncqi=-WW$dW7+mya_X}&`tWQn-0qKsft~lF9E$uS>LeTy$`6kf(GsqE!K)31o$;z@B1sylonl_$pN1J zOLS2uh_KtPdkZQ3Ytlwk#1!{z>p4x7o`h%_-T}rCPS)>FS}*%FiQ$Vyru3B1!melG z(yB!cTJcHl4(dFG0cU*>B+O%h$h>x(T`Nm6Ys_*?ZW-)@y!czA<;qsjv=Yz(GBz^VCB2ugFK+J_O~KpKRnlcIcjueD*N0eSUb1s> zty1amc)oo3p?__CD65M<)qZ=XMvXspZ}BTG1GZFD!2gUEoN}b#-;biArcTbv%1TTe zottB#rtbdfx#0)FQ}Hr4H_w(uK<1Tuwi7utUx$akx;mP|rTNm*(&S|7>aeh)xGkMu zN>(!@HPmT1(N1z-$-9pBu-i$W%TTU7?nkc0Yv-K&#p(rtfW@P~lXN{ss6Nd))13jS z!(rNF8_@O4VXf(omcxVe*N$M$ zF595ysK!|grq~(Ax+ysJNr6puXDp5^){f=dBU7*sbk0bya`aabLspxJ9xRZ;OZ*5m5x3J|pI zj?T`0u+7KvRvsLBy(IX)shxAprvI-@L1>=jGzrVi>uYeIGc+^X+TE2!ocjQkRaFnS zq-A87jJ`WX;#5>ihmw*a_2ri+C>C0pL#V9U7A`E-gbdZ4C=1oun@?JhMZ^v^{U+ode4MIJop)SbqOHp?(`(&XbFUD!ZuT+1dEZ{%MJ& z4AICmAfF_Wp#!WrF)nG6NWv32g7KXS8*lYC=}BPstCeGtLQ3oo#yF0L4Y?%1GdN6j z^btFWzgkn5-1Mmm3#aB=q*n~2x83!Xl_LyMeEj_Uyu3c%-gAv!Y_h$qyu8o2seiAn zp}&78j_ee3og^>7zjbQ@=4)y?TV>aSOQ^*cSNmOLLdCeb>DgImmb5SKTRLxXUuZts zz~s+0zc({rS^tZ}BM^8JVA-Uy}5V{wTvTJ=8=&K>=k< z#J8E~=;#`!;mL^!m%3S(u|oIh%COR{%Nq-p%>gkoBHPFdenh<$_9f-%F4j~Yqo6=d zP8tT|7=r6y7%t-??B2?DAcK^;)Mx< zu5yPmoeUd5kMP=^@?x Xl%7gson literal 0 HcmV?d00001 diff --git a/reactics-gui/resources/help/img/ctx-automaton-state.png b/reactics-gui/resources/help/img/ctx-automaton-state.png new file mode 100644 index 0000000000000000000000000000000000000000..fbafe425d14eec1d1ec0ee76b5d23eed0329860f GIT binary patch literal 5242 zcmeI0XH-+!7RT?d+N~i$>hz|mxcO@bqB!m!JAO#{ImJuU1dJ}_y0s;b} zB4SV$%202S2gv z5C8xX8*8L1cy$9`K>}RhyHnw&4tPn3c1KfO{h}b@Bw_#|1P7s<2**KiG(rFX(1s3Q zZ5L_O5_e}u?A{w?O4PN9zOi1VmCzvhbc3i@C<#{T_F0hvm+%!}F2{fOp= z@_7pDQX1moSss4?fFKV6ObYE_kH8W`HU0dF7@Q_8G#tzp08Gqi;eOa)90h{G;R#`; z(0OJ(6hiPfg?i{aXgP#i-~tKO(IlK(w4*yVIv8u@4>da|XhK7P0--pHAA}Yf5=KVQ zOrc+N5#ZiVA`5mu)n)g2m$}aecSTgeLEQ8 zOrYUH&`3fkE{qJOU$VWWCe#m)^C0+B0>4FlAGgL4@PXhw z{v*PPM8JUrw&x03ps;O@u&*G&b%A|bm~A@$`{U=2{1D@xxPIdLAp$?-{Ij}#;`$*1 zKji$gy8gd#34U+waA9CS7X>zM7P=EGu<7F_o7=bx2nf8Ia2f}I9an6S|8S=b&E*8U zyLs$scCvnEp>DI&`ZuS2ye>&qXV+DKS-isYqCn1BqR`#b#stK;x4yM#tD=!IoxR+pb?rh^Q&U@eJDE%_D=XvWI)heknh4Lx$Y{@m z6+5fSz(czG`z>XSf~M`Q@}0HzUVik*FeWC($;s*1v13^5>v$naTV?Tl=N8Vg+JOV5 zrKN#-o=7B*C_P7oEh|d5EgTvg>mV{sSOPc z8X6j&IqbTs5A5k_N9oYQ?3^4h-4ttOkVA1XtFP}lrb^x{?v594(LNT76%`Tjn}){7 z!%!Kn=?#W)6gaPc-F9_#Rlm+nGxI)Ly$XHD(Kj&gc8Aa_8ElxZFC?|~MT3g6G60-Ee|~6aNKi;< zBlfAYD#(g1DtGM&EZKU2W}?$H+}Maz7Vn6CewJ5gc5bf3y>tod=9Y@UMMc%b$Mfp6 zl$V!-fmQ@Su<(HA?LIJwpP%19i8y%Avewq=3K^a=GCB(8GDR}VYIR+k+)q_vFd0)S8&+XmAZ3+t@r@|G?pJ zSnN$}<&^d*K0ZDqw5O*hV&pM(MxHJuC1ofps(r#3INcFIkBlnnYHBK2Bh~f0 zjYN!+t?eBgu3Wu3y+|V(4<#fdK$G8m*jPUFSLmkh9wKqxE>n|X7%{oA%#lWjCm>y1 zT&%3DE~uKFJzieZ7pMmg6}sYEEO0tfsjcd&suwO_zAm;Jc^FXZLT6}t&rD5K`?rcK zDJfZ4SR^2O$HvBbdtE`1qepEDT{-n~H~w;Y515$5tKn%b>5oBIs9LUSVdCM2^(RxS?K+^h64l(09` zr?b1{Gq{24-YhJY8u56)p@)PDYgM8-e8zW_`CPp&a#y^$hTbz6_2`q6#Jjmq&mba# zpSSmZu#Y3l9m>C;fR5RCM-7i;3|;BIFz?Rdk+@&ZEE(%1kd3=g=cj*E(nWL;GVgKe1@4m%#W|BWpF-iC9(@uBCBh_bClO;uW;lbDma!~Oy+6v z!?l??$=h}4+D>E6QmtpFlCAUYYb6w_eg1;b=Cgs7lfdb&QC~;ive|%_ZPlZ?Ccgnd z(R4yfd6uT|$zUbnIkC~{xWT5M|7Q5#loecnb(%70m{|L)& z9~eMSRHt1`$?2%ppJ_DE%$W`f7d0ebaRZN5VWSUK zZYn9gso6j^gtT;_PMv&zNVwn6f{o?L7w-l9&LNKGbaTE4Y_^m@X0+E{hs=gsX?7@X##-UVYOPu z$I6CJKK*@6=I=Mi8+Ccrg#2B(vl2;}Yfgvz+^a~XnZJ5*;B`suw`f>5nUtH%_o8;M z#8g&GYad?oPU|3+pz1R4{}N#=^f))7NohZiL_nJOKXP- zJ^`nQT_yhef$?8CE<2WkqWH%y+9G9j^A!I}yUiHOjkgK21+tZLG2o*!Snk~=T{EKX)WjdLz2ko(?i9ASk+Nd3qEM*kP`FH-k#1l~%)!bQgH8UAD>ojfytkwC@hfwm zT-84;`8rW8$E1dT_|NsK!gm{YynbvB8qY3PDd^cNbgY+e z%qiVrt+T8yGWHr{^JG2x+;RWM`llo3nrRw}bQKY;n0U4p@rD+DTFU4{z4SKx?QQYf d9_bY`SD)#q8UyD`w*mV!z{b)MSz+#b_MhsQ#gqU5 literal 0 HcmV?d00001 diff --git a/reactics-gui/resources/help/img/ctx-automaton-transition-edit.png b/reactics-gui/resources/help/img/ctx-automaton-transition-edit.png new file mode 100644 index 0000000000000000000000000000000000000000..888e93da73a94bb6d5706ab6c23e883203d1eb46 GIT binary patch literal 12138 zcmZ{K1z41A&@Nasf*_4b2oeI4(n<>w0us_lx3I7@#!3j1A0j0!-Q5ZzUD6UO(z$fU z8NNTx|DWqR>*dSl`^3!LGjrchkeZ4-5k3t*78VxK69pM{EUZgL@VpB55?s|U-_nIY zmtCZuXyW4Hj!&!pftU9XvN{N9XLA#TwWGrwO>28|EF{8_^A0c19eWcS_`@r}d57nr z$OC>6KE81>hZ|T}cd(wwJl1qiSer!Zkhh-WY*aVBu}Wv7A$WV2MauLFxf1{Iz2U+S z0+KI-scMU5zu&McPL@;dGk!w&Qz7uRF-DF^=MMWl84}HJxF2w7I?7K^AGFtu)#`z6q%P z!liVzDdk1}FbzHF9c-*`5AjfP-HZ1qf~(_4FH`$_(9?SqhaYn|k`>;5az;x-%7TrR z9Jkp-Tbo?o*mh0U-=qpV(jm1~5sxA6joS8eZSBb9V_Yn(pO33%+J4HGzfh+9Vfujf zj(}Wi5e>gi$EeuMrJ1_Hn>Z|{?64(;`+`s3BH(#Xgg zG7?x=S+8UmBQi3~>pgdWmsxLr$GKf*JEFo#p~QT{!7q#`%CuN#XL*Rjfzymqll{4t z)^LUW_$_fy=9o@dMn(#yQ6_9GEE@`%zf}HhX1tb`3$c8bf({cpj1hf2PelJ&eVdh> z{F;({scCJzawK0*TVJ0uLV+Cry?XYnL^`;RT4^7HR<@>%iAjojc3xiICr;h1^;*oY z{AwsVB4Xba)-$p7UejFhgKo~ z*hqw=sb^O>qPb!^tz-K8GQoOk?TU(u>FR6@%=hkD4dpzqlh=d$e5R$bZru!%JZo!f zQ_I%G{fLESob!)j2K-Z1ZS>e?@zRbs{p|mFAC;q+QR98+{OlR&HBB&hS^M19-@ku5 zW4KF6!#@V88={}(Yq7Gja**Ro$53NoC3moqe@IVfromqNyexS;aCQ=@nXTEIB-vV; z4Py{f`Fot52s`RT`=KM)+1Ys!*07qKCvbaiVqU`Sqg=#j1CzuE_=LqM+aUbRbnpap@JggIjX93gD3s;LolTu;?x54$bNP^9;qGKAz;)vK9&y~c{Nvh+ql$0;$%bJ>h^I}?*) zo9C~CgF9#2qfAXr`&G(q2D6@JswCnvm=?SLz)eCvRW)W2Kfj#3xVR{pg4`;xasu?foMD9+`WMNj|iwtPElY8#`C-BMl#N zec}2ovAlo&!6Bjw{(<^`@ZM zRSW4DvJg$DjrG1h9;v|h?{~%>8yQePT3ay_)K4oVymf>lk~Kx$Rws&ITAHtE1?lT2 z;4v&MEx{5PQDznvT8bsGkcp~uCe)9Xmb-WFK39xm;pXPXj26#GNHpUR(;YNlmzKB%1#C0kA$m)t`<}P0t1I1a)0~&uKtoN< zX`zR{W+GD+^F`dNrt0BHuC^-k4RdpIJC&7}M=PZ3>gx9Q_cxy0kV6Lu3JPj`_5NM$!s_L99K&s7VPR2V zSTD%I!SV1wRC`3w@9c0P{Yg@Z`N~A~Kr}}TE<<*9_DriPGsNepATS= znwol@9^W#Uq3HQR2k!Q^9%Hm36BCmoT7_h))VpPUIDZAK%I`Q;S5&mPG(hL@_Sv&% zuwEB{5mKt+Y%WR0s2rhZ>8?AG?yoRXBn{`zEfKvmU4@W9TF4jXjC zZ9Ilt?LudyqrA}A`1ttm-wp21&c@wUR8+k7R!b@>&V;yQ03;z?xb!L#8rE{Ncrxa5 zcWYj0Y-}w*!Zo3qKiZ{5C|5cdjO6Kd_sAK7TYb8(S7A5ie7xrfJ5tUvTC=P7_%Zqg z7%{p#UMNWvsS?GaTw!+@N5WWlu_+J)t3$b&(b3OgJ{cJqvU0a1Jhoek#Dt24g~hFd9G#GmX;Yqq#7w!&cU6>^ zzd|}9r<-K=!T~G1H(Me-cj>eW2%VgqsCdmbu1l_#78O~ItoukQAa)|YeN!&C)f2K` zzDPGJ4d?Ag%R{-HpYrdVPf7Mo*tbWv3=a>>%F5CTU6XL%Fg`ihyzM)hFCVsUP=lyO zEU8~5XpWAI*u%Y#aqxrri zY&0GHN@=471fAtVSK_h9`Pr1X*Ph)}-C>bPppJTM*f|f8%lqoaiYveR`#Xy*`&yEDDDR}U3`MzTVn3t z&W`rcenM7#$&Tm-aJ={L&k;e34;gZ+s+hsunV4pp-Ul}aTz5er%8H8A?vam;jSeW4yv;}He7ya`=!D;%?#4Sdh&%mR7_TIA zK&y<_9j<`shZ`G_$9roRzzjIGKIvs8u6r7s_~py`?5xZME=b+}r1G?`S?NAE=BgL= zcT~CkxLbGJ(An7;{`*Mc;;AZ9?O_@BS85%#BY{|W(QQplrrYz6u3x`CL zZf|F|y0(^Ez%$pT9i_m`m{8HqwRj%gw!19cca=5stBQ(pHAD`QJYKusdJV*`>>vcjR_kB-~0GQV&kHso%`3%pSU|sq%d)U*DV5 z7#<(5*XS!gO}@2Fuqb6VI}PjKst~jrRWr_InTj^?Io%yDY@F&CuXbIjgr7(rEi!p( zsBvj0h`5R{GNumdE8cf|ca3QA(rI3>mYZ7zYGCb}#@xa}FIQ{p`Qv6Y;gf}iv;rcm zo7%Zr_iMsqVzkxO86y-r5C_SRFFQ`w`0Os1g9|h@NkQ2*x4N2Ft*4?A8Wp7xFK90& zE`Ce$th2v=bG|#i&Igj4+sg1-g*|!&-FTiTiX0diU{y(YB>F(RKtKCOlcr|_Dm*0Q zsg%O$(XPF{y4UWGE>YARc_w-M41j-{D+ONK6Fu+1Xjr5Yd4OcR;() zu;r)W&8ZwqhVqhKNJ*!9hB?Jz4D9nA%d-FX#1J3IT4_HuJ`c}QELmvnK>xU$WvciyDw(4c8*%2;16==2Ax zMlN3qGrm6)NSX%lGSztg+IFOXOp3~%jgxaQx-DO?l12GwXE1x9y1JS@I;W_J=kDFz zv(w`vyZk_Cbq){j*ZZEz9iD9uXO3F-BwW zUoRKQSX*1;zn9{Q8PKlQm$3iMpP_EO_!j${EyQqwD3X}L?BpN_Qa;SWpwyxpS}8p> zwT&K8M{a{M9tZndmW+%HF|A-%d-hV(djfBtOy2{O%4cbE&PZb_i;)6xfA%k=aSvX4 z!tNPD8GgE-Atrn^Ir{S-L#EgLQJr&2F`{y(qQeik=-m!J(1mPSLH`TF`rv-zJ_)nlL5fa|xlT!i6Qgl~K1 zn$pBY&UQzPp6gS=J86C8w%Xm%{|@m-8gT^+>wjJOPEJDK)HV|uT=}E7v4p!`n8n0| z65&;y*TB^A<@@@Fg`&cjqFSkIa5rA`eIe2g0xKU0rTF zND1vCTdw~=^#t)_P4#7f2(NDz(>BVpkntxeeTI3~WLt1$P66}RWxv}M`NsI>IZQmb zgApE5_1dH}fuZJf)KvZ3r|j%OPw+*NrGH;?Q`JBCuN%nSpzqvkye@a6Bj>L+;mE{) z4fXlVe626VCxCdZvnD$ZFXo4PhwjZPOUo`xn;uuQp04~UWlTs%_r0S~{OB6GV~DZq zs~7`KO)GnQpV?77h}JFhl`u>o2>yylL_1&!1nFX-Ag$EQLiywVm79uP+;D96I;5w~y6xJQNgUId2Ju zkg2d6vgsTdXaD>)=t1OS+dnVQgDL$u*x8v;?+cX8??0E-ucGVh zjHu14F3)54<(gA@L(woOv&b^Nq860F9*|Rz_90h+9{O7i)=)?NM!^N^o`QNwEr;*y z^vj94bk&mG?T2<9%++;f#phf51DI+t0al_?>2uy<%a9JIX@v$0FkZ%x^j{aC4sOK|SJbNrJ)wV>?=%THTm`f>o zC)zj(UBA8knuyz(@$!x?RD^Yj5TbmRF}g04RW(rHJgM=r96_SLW_Na~Z!VSJ z@ut^d(Urfcog#AMiNxxd<;+oe*e!|lB_2YT6Dx$7`>0Xa?GYs61g)0z_?(vIMv%Lu ziM9FM>|ovYhS$for_CS_nEgzK&SyO1K0hj7bX0!<9j4A*prs&E6#Xz_BM2B zRhTTb?A`N}XMe9wPG_DTGd4GS?yb|h9sKx{A~C^v zMX*@1wa4)5N?2mO_v)&-poWw}Qp0I;s!9<@(!!kmc(u^UVyr65;Vn^T_Yvgdi9|1- zLGIO!Adlb^Oy*a+-y1h4%iM-Op!9?m{H7cCGmBD~Yw5Gq28mwVtQok#< zljDiy{T=c27k;Ihw{er+MyxdWtbAR}QdobcArW8gag4m%(!#cXM#n$M>SU|twimUg zCq$rsWkqP&ZE^I_*QO)M?<`v_o7<=+U6Z|D#I?9UL;H^CpjXDoae3|o6v_2Ml}nCz z(|o^Nt9PbWBuV%**EBv+7x3 zt%W6Kqrl7Sy`q7QTa)DnPwuE1!3vLFm!!G*;atqU@UP#fmumFQbL5#U$@`z_{)H_a%;Vqr2P-KIUT!|6b3VPHFRu4T z*Vap)vWD?hXZ}$`7Y}-OdcGHk7QNbiStvG?BOogLX+nj-yZ@NX`iwrIS(P=)} z`j{trVZ@Xww;NyW?oUm_BlTzDm+@u$%#PvU~7ANaO4a`%MNJ z&hmSlTxT9=u65$N#Og-h@{{0yX49{IjIXKKy@S$eGmAUMU6{((HkxAF*}BF2pAn(3 zAj^?Yfhv55H}dSTzkY8rMgoEXb&U#p zeS@$6;zC~QRwCfShlaGAkhCsst^@`YEH+rYNMppXIHt#_+Ue{0x!iRsK|x5WN((B9 zfg(RTrHsi&iXM7jDfa}(F8B5~^7m4$}eoo1izPua}yxs?=@ z_UXe;gc8MN=Uv4~Kn?1(VPo^$+ zy!7nwY?1Oily&hR;vFK@6o68SH_3BEY=C_TdI)+^HxLB~2nhCu9v+1*mwZ%=arMhO zxY;Zq^goNLVT@qpvn87J|5a5{$s#mAz0wpB-hDho{=+PK7hhWzUu{TDejabvP&R~7 z}&Pp z(2(29ZDJ`?xq;JZFI|1Ju6E$Knw|W|D6S!Y<7c6K4Z%-kfHZfAga{i=XY%*VmtjV3LPU5!k5voSb%ccJP)~fxhl{ zGixPLpCd$zl1|VQY^wb2h2GnezG4Cbbg0fQ!q6sQzY5LQlkY@7_H| z#-{OcuYs@1p`oFwNfOG+${#~R1rgO)UAWCWE5rGs$n}Jx zjkPHYqW*qkl_UvzQqulxjZBa2`F??qGy)ftJ#eF=J|KqdVbDpDky5zUVkQH8PM*^wN8&THv60~Z(YMyk+#0)2>?swZrQ2DPQ7 z<<?W!roL;Oh4P=hZ=~X)1*C~3GqP7ZLe`b=e=XSTy z>FMdxux_b^04N}L@6H`;&Y;2<7Z(Qy2Py8q=!z3ivQ@|WifUL3Afjcdi&tR2G5SJB zr^;)89liw3|1D8BJD9*keo9J8sb#N(_W_T+%;x6i%1B{lY3X<^5))(O3%q+je$o|9 z2^sl!PgGS|QT(>UPe+Iu7#M8Ie~*k*0$BidZ)j++Dfc`-JDu>E?@1g_l_jvXwf$WI zrbc9dY9%)^+Z!Jpy$jOCV1a=bP+7dO zc_k_o->kqGfh51upOCpJ-zIj;a6-@tIp{-oY{pBy_Uh-4A5N9NAR*j;QAQGce(0q% zo>*8|n0E1)`G-w|9b=dL%h+tlJ>%=w8&YvXjw*hxuU;{r`krZNb$+_P^fo#gGD(Ws zqT(8`Fenlu^tm@}Cy)wDQZqk4E&#D*Gn50nTMr^#%ZHobnmKu7*gU=z6cnqxYtu{T zB-X%Y0_ALK`Zt)8d(cMUUq*O>-fG4inDJNITNQ639wGRtfC>ci0=n3mnwsU(#$i8$ z4E5}9TFQ-QN4XzAejHX778XX4{5CR6V|m@4cK?BZ!1LZu3b@bMqbH0;3XPJ&!+C)8 z2JRtPhSAZ{k%mdvPIO4I_b0&+Aye)(KA^0n6s)YW3h1pG!_VT|xyo#Y6q9}kfJETf zsEk_;jQjAZhPwLR>ex$1$MbF>^uvb_z0Xhg%L=mv*swHso&G$MYI}1ThswXdJPf4R ze@Vw3ZIOcJR3;Ii!GKFoo+)dxvW%G0V@MDrmb(gp3y8vpSnT`!`7`JQmgeSc(H*O+ zs~p+|oG;1(*LfT!9v17=0hy5i#Jy_L`tNcjPKtB%`Dv0w5KJt}&oN64A`gVo@87?- zx3>ewNli`N8cHAk;N>-j^sFqa-Q^+04Cju2*x?doYYoq0AVPdlj3qV1|#LbKr zzrtE@UwMf-3VzDP)WGzEOu7H1_%5CiL zb8~Vc;NjvDFYYDCU;`$ayK?umlJD5#}>TY?3mF7Z47qc1_Q z1K|#2i-DS&v5CpES~q)bZSB3#KdG|8!2CA>=P50nn3&iaLS1Sz#J;z2m4E^S17RMX zzMdWjh}}AzP5}>hcTWAPaKSZ@vk8I72eIn8yQdmgYFQb7wSIxxz0nZ>J0faHuWl)$ zr<7P~_K<;6F7k{>)MniK1^`(QCBxgzE?l2OP78$P0}}fG_X>F`E+$4EqjTxe?xVEJ zJhw#B(h?IV;rBHammbY+p{YXTaMTh{gz$YHme^5ykO*ft4QlS2E-pA;@yg%1Pql@0iaTpnz1ZC&V!<@3B% z?y}GW{AtV2pZKdTGe({Tg|~`}i+z24A@}ertQ*_esHI)bs=l&ruDOq#Tcq~-J2N9> zH(KO8*8%$tJgV(ji8;s-j^h>f**Np_^MLOWiELl5kp{N_N8HohEr59ZZBWw{mh~h< zhScrzGncmhfdM{dX0vavu>q#45KA{|&meyQowqzuy=|G~^D}Yz@rdz!OE9I6w|5O< ziP!oU^IoSI$i@%BlfeeS^wq+|`7F8~x^E;)EHv{Fa`P{pVM>HVBBv^urm9_9Cnpn0oaeh@0Xjh4q65{NJ-TEj zV|scTaG>#IOG!bY4ayUKzDNaT=juA|_g4mt?LMk}w(vlqPasu6>H*Hz(~t=3-4i7x zB@mJn6as^TgFk*eh3u|xU~nqv-Rk7-?#@F41p`z${3E6K1O&B+rBn}c%m_?uVD9AP z1df{YnS*woq2A8Zb+o%e?f>i^InXiwdlF+ce2^qXSNI~>9_2rM-mf~ky7?8(-=n0k;5Aa1^~M_C65 z#()9_4r3*E>D643$gt2*7Su$YM-=e_2&$n}58jeQf+99EBaNHl`b{O`b8Kw8vOHfJ z6k=SuC1!A(#ozNGZb-s20g?Q<{@wZBwl)&q?aNfr__Fd)c2C8Dwq1$#_3BTR-P_v( zGeH%U!ICOWp@>^tS?PDQV-1qnQX$lX8Ks0a_1cdwKY9A}DO7FX^N>0;BDNNRP-GJl z+TWaM{q*URbG4YL=rJ(&%JG7CQGqh4aKCo5l9I2~baZu2(@iPT0a~WQ-~Z9{OXINh z=s2Cn;bHd_A7_hDSai9Uq4@M^0i;oUV_X{52)NcIO>`r3Y=q-~N`hc#|F?$a`;9 z*XLFy!p$x8!v}UYwrU7Uh|NxeJV0|$UBv|j_dv`H4GO};$EOkZL}bgumIv?S$X1Ct z*6(V8@;dKfU2vPn_!|He6wUAeF>|WX&#z``a#9>>?ty_)m?=cfP6VA)8&t;)N6Wbo z_<+$rTU&b*grf>>L-avtyEr?45%Vaq9~bP_fFnuekSBJZexIe*OB*=X<3-dT!buw` z^a-fE7biTbJMq-ScW870_tv2R{={XFqm}y}6OgY{YznCu5Yl$EXc~}ip*voFWc!O^ zCc&jA)wQ+UIz`4{bI58A6IGj#o~HcHeSAJBN|Jx~&63vk$a+seSpfHdV-AGPP6TPy zzL1?D=flYwX4KBwc+6=oEM^mqJ^)nsn=D>3Kttfw)rm<;HbMn)afAqDH$*+O67arU zC>>k0BBV{9?RjMfk3pOAVFqpks~wb@aX8;l`FIJ^M;MSlYQoFv;ZnNH~~<#)7IR9V`6J) zX6>PC0Q*p=Nyns$+2}vS!QwH2?6@&_3rlUOE2n>#e$G~Ffj}U%XVFTl@(~tc&jhq_ zRCM#mLG^207~J{G=zStJ;-8|8Gtm4>9L`3SSbRLB|IR;{EQezpnNy3&@>?B)YysUz zN1Vhw^2(p=<%>^35WezK3QkT%0Ri&5y#e1(Le-jwlH~&6w2g)rwy$h((hjUfR5^U+Q5rjFrBa86&8?#SGPsq#^#>M zX%BB*+=a+fR$gQ%LE=99g9oo*kD)h0g@1S|kQw|a>_ZQx%6fq1v{O1Q&Vp}PUv&Wq zl@OE2JW}%>dEB;WiH2Lz;z_8TNSx)HL;5$oU*xp4YNk$L@^6GBUq5^B>yW+^2Zn3s zsrYy96I3wwiOI#cU-qYY8ks)((+n=UUp#@$vf|`vOpE2K#OSu1gc>`2Mi*OrI|+r8 zkj;asOt3RpuRp-Luzoh>(a^(7CRiGF$lK~klGT-+x$vz4`+~;3!zHseVGL@0s_1T)U8+dOnTq%YfFzDEtAsHdd+o2 zgQeg|M*5Kp&P$DVH1w~ZUtktmu17C{j(p}>poFX-arWaG1wL;K%lP)`>+iCnDw z&A*5bj$%v`;_2HO5)vZpGLOJa`M|Lz1QBc)pZ4j;g1otZzp>+45v3xK+4}|dM&s+# zS58hOK{7WJY}S8%q=jLrprwXWBV&G&j#kn_{fG3o{~LKu(w4onTx>?08C(I1U1-wlMgn;?{s$rTISwF(U?RI#oI91r~btP7mJzy z3I3>G=|IoGeCOiv+5qI(L!l{m>8h-YuSpZxAjB@7T%JerQ+!7Ecg2qH=b6HGfyH(B zVBfH?W=w4QNnvQLM=h|gST9YqJ`%&o5d+lpl-?q#BArm~s&zwMy!2bM`IZ5^%DNT^ zZiVIj|GSz>;hyrIIs4s}1T_=ykDT<*|0tQyfi&?|g~y>2D$H=-!#=|IrrqWK zT=3#i`LB?7rt1p1I-GK^K?*HRrN)+JB=s|U&iQlyGJM&?M0#e$D)1PlZ9HE#fi$a) z`s+ts6Al9oefapg@FgR%?&gK~+C{?64>SqeerTEw=O+c`)ju|W)_IyKDB&1tPLK>^ zkWACHHow#~oy!bn-!qw@@f+sc5kSPkuH+QK)e+KD!yI#MM4j(c%_m&hGE%nKdf z@QdW$bhu*13pmCSq{&G!aEBF=KF9PGVTWa#@)wK|Swl7sRx%gb@5^Kk5$9I$QU?@b20RDm#5KQ zxPKX8nsh>PTd7R@1JrR3B57%i_UVJ<+{uDu*rPxEl&!#It%Nd30c}TxM`|g;p5Onh zl&qar>ogOS70V^WzjaM>>}o104JjO7{`Q(5M?2_eOo%N}cw8sg%oPg{RMHXtm+A8*{}8>g zD~yuxXFA%~9ai`Hi2DJSq{$zkQ@(e{!z8j+PBF~vGJ`=U524STM9+uNi#ZDW)P%ig eW_CP0$9@+SrXaB~l>~;sdLpYLQy^vh_WuB*H$@!) literal 0 HcmV?d00001 diff --git a/reactics-gui/resources/help/index.html b/reactics-gui/resources/help/index.html new file mode 100644 index 0000000..d40c9a4 --- /dev/null +++ b/reactics-gui/resources/help/index.html @@ -0,0 +1,321 @@ + + + + + ReactICS GUI Help + + + +
+

ReactICS - Distributed Reaction Systems Model Checker

+
+ + +

+ ReactICS is a toolkit that allows for verification of Reaction Systems. + The toolkit consists of two separate modules implementing: +

    +
  • Methods using binary decision diagrams (BDD) + for storing and manipulating the state space of the verified system.
    • +
  • Methods translating the verification problems into satisfiability modulo theories (SMT).
    • +
+

+

+ ReactICS GUI offers a graphical user interface allowing for editing the reaction system details + and model checking using BDD module. +

+

+ More on ReactICS can be found at The Reactics Webpage. +

+ +
+
+

Table of contents

+ +
+ + +
+

Reaction Systems

 +
+ +

+ Reaction Systems are a formalism inspired by the functioning of living cells. + They allow for specifying and analysing computational processes in which reactions operate on sets of molecules. +

+ +

+ The behaviour of a reaction system is determined by the interactions of its reactions, which are based on + the mechanisms of facilitation and inhibition. + The formal treatment of reaction systems is qualitative and there is no direct representation of the number + of molecules involved in reactions. +

+ +

+ A Distributed Reaction System is a computational model in which multiple autonomous processes (aka. agents) + interact locally through rule-based reactions. + Each agent operates independently (without any central controller—coordination), + processing inputs and producing outputs based on predefined reactions, + and their collective behavior leads to complex system dynamics. +

+ +

+ More on reaction system can be found at The Reaction System Webpage +

+ +
Back to top
+
+ +
+

Application functions

 +
+ +

+ ReactICS GUI allows to: +

    +
  • Edit the reaction system structure (the number of processes/agents, reactions for each process/agent, etc.)
    • +
  • Edit the context automaton structure (adding/removing states and transitions, + edit context for active processes/agents, setting guards for transitions, etc.).
    • +
  • Preview of the state space represented as a transition system.
    • +
  • Verification of properties defined by formulas using rsCTLK semantics.
    • +
  • Save/load the reaction system structure to/from XML file.
    • +
  • Export/import the reaction system to/from RSSL file.
    • +
  • Export the reaction system structure and behaviour to ISPL file.
    • +
+

+ +
Back to top
+ +
+ + +
+

Distributed reaction system editor

 +
+ + +

+ The structure of distributed reaction system can be edited using the following buttons from the distributed reaction system control panel: +

+
    +
  • New process - Creates a new empty process.
    • +
  • Remove - Removes selected processes.
    • +
  • Copy - Makes copies of selected processes (together with all reactions).
    • +
  • Rename - Renames a selected process. Note that process names should be unique.
    • +
  • Move up - Moves selected process up the list of all processes.
    • +
  • Move down - Moves selected process down the list of all processes.
    • +
+

+ +

+ The details of a single process can be edited using the following buttons in the process panel: +

+
    +
  • Add reaction - Creates a new reaction. The details of the reaction should be specified in dialog shown below.
    • +
  • Edit reaction - Allows to edit the details of a selected reaction using dialog shown below.
    • +
  • Remove reaction - Removes a selected reaction.
    • + +
+

+
+

+ Verification of formulas against a system specification is done after selecting desired formulas + and clicking Evaluate button. + The result of the verification (True/False), as well as time and memory used are presented next to each verified formula. +

+
+

+ Clicking the Reset button resets the status of the model checking. + Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure) + the results of model checking, if any, are reset automatically. +

+ + +
Back to top
+ +
+ + +
+

Context automaton editor

 +
+ +

+ To create or edit the context automaton structure a proper edit mode should be set using the edit mode panel. +

+
+
+ +

+ The type of the newly created object (state or edge) is set by checking the proper toggle button. + With no button checked, one can transform the net by moving states around, etc. + (see below for more details). +

+ +
+ +

States

+ +

+ A new state is created by left-clicking the edit area (the main part of the component). + As it is customary in automata theory, states are numbered separately starting from 1. + The types of states are distinguished by shape and colour: + the initial state is depicted as a square, all other states are depicted as circles. + Moreover, hovering the mouse above a state allows to see its full description containing both + its name and its (distinct) number. +

+
+
+ +

+ The details of a state can be edited by right-clicking the existing + state and choosing the right option from the popup menu: +

    +
  • Set as initial - Makes the selected state the initial state of the context automaton.
    • +
  • Set label - Allows to set the custom label for the selected state. Note that state labels have to be unique.
    • +
+

+
+
+ +

Edges

+ +

+ A directed edge between two states is created by left-clicking both its endpoints in correct order. + Each edge may contain several transitions, each of them defined by a context (additional entities + provided for active processes/agents) and a guard (a condition required by the transition to execute). + The list of transitions may be edited by right-clicking the existing + edge and choosing the Nondeterministic transitions popup menu. +

+
+

+ Hovering the mouse above an edge allows to see the full list of transitions + including context and guards. +

+
+ +
+ +

Removing context automaton elements

+ +

+ Switching the toggle button Delete on allows removing context automaton elements. + Each left-clicked element is removed from the automaton grapn. + Moreover, the entire context automaton graph may be deleted by clicking the Clear button. +

+ +
+ +

Transforming the context automaton graph

+ +

+ Any state of the automaton may be picked and dragged around the edit area to obtain the desired graph shape. + It is also possible to select multiple states and move them together at the same time. + After CTRL + left-click on a particular state the entire automaton graph is shifted to be centered + on the clicked state. + Checking the Lock relative nodes positions checkbox locks the relative positions of the states. + In that case, dragging a single state moves the entire automaton graph. + Moreover, using mouse scroll the automaton graph view can be zoomed in and out. +

+ +
Back to top
+ +
+ + +
+

Transition system viewer

 +
+ +

+ The component offers the visualisation of the transition system representing the state space of the reaction systems. + The initial state is depicted as a square, all other states are depicted as circles. + There is a directed edge connecting the state Si to the state Sj + if Sf is reachable from Si by a single computation step of the reaction system. +

+ +

+ The component has two separate instances represented by two separate tabs in the application window. + The first visualises the complete state space of the reaction system, + where each state is represented by sets of entities possessed by each agent and the current context automaton state. + The second visualises the compressed state space, where context automaton states are ignored + (states are represented only by the sets of entities possessed by each agent). +

+ +

+ Computation is done by pressing Update transition system button. + The reaction system structure should be loaded from the file or edited manually for the computation to be possible. +

+ +

+ Note that no matter in which component the Update transition system button + is pressed, the transition system structure will be updated in both. +

+ +

+ Hovering the mouse above a state allows to see its full description: entities possessed by each process/agent + and the context automaton state (not present in the case of the compressed graph). +

+
+ +
+ +

Transforming the transition system graph

+ +

+ Any state of the transition system may be picked and dragged around the edit area to obtain the desired graph shape. + It is also possible to select multiple states and move them together at the same time. + After CTRL + left-click on a particular state the entire transition system graph is shifted to be centered + on the clicked state. + Checking the Lock relative nodes positions checkbox locks the relative positions of the states. + In that case, dragging a single state moves the entire transition system graph. + Moreover, using mouse scroll the transition system graph view can be zoomed in and out. +

+ +
Back to top
+ +
+ +
+

Model checking

 +
+ +

+Model checking is handled by the component at the bottom of the application window. +The properties of the analysed system are expressed as formulas following rsCTLK syntax. +

+

+The list of formulas may be modified using the following buttons: +

    +
  • Add formula - Creates an empty formula. The details of the formula should be specified in dialog shown below.
    • +
  • Edit formula - Allows to edit the details of a selected formula using dialog shown below.
    • +
  • Remove formulas - Removes selected formulas.
    • + +
+

+
+

+Verification of formulas against a system specification is done after selecting desired formulas +and clicking Evaluate button. +The result of the verification (True/False), as well as time and memory used are presented next to each verified formula. +

+
+

+Clicking the Reset button resets the status of the model checking. +Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure) +the results of model checking, if any, are reset automatically. +

+ +
Back to top
+ +
+
+ + \ No newline at end of file diff --git a/reactics-gui/src/META-INF/MANIFEST.MF b/reactics-gui/src/META-INF/MANIFEST.MF new file mode 100644 index 0000000..b010a96 --- /dev/null +++ b/reactics-gui/src/META-INF/MANIFEST.MF @@ -0,0 +1,3 @@ +Manifest-Version: 1.0 +Main-Class: pl.umk.mat.martinp.reactics.ReacticsGUI + diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java new file mode 100644 index 0000000..4c1ee59 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonEditor.java @@ -0,0 +1,693 @@ +package pl.umk.mat.martinp.reactics; + +import edu.uci.ics.jung.algorithms.layout.FRLayout; +import edu.uci.ics.jung.algorithms.layout.GraphElementAccessor; +import edu.uci.ics.jung.algorithms.layout.Layout; +import edu.uci.ics.jung.algorithms.layout.StaticLayout; +import edu.uci.ics.jung.algorithms.layout.util.Relaxer; +import edu.uci.ics.jung.graph.Graph; +import edu.uci.ics.jung.graph.util.Context; +import edu.uci.ics.jung.graph.util.Pair; +import edu.uci.ics.jung.visualization.VisualizationViewer; +import edu.uci.ics.jung.visualization.control.DefaultModalGraphMouse; +import edu.uci.ics.jung.visualization.control.ModalGraphMouse; +import edu.uci.ics.jung.visualization.decorators.EdgeShape; +import edu.uci.ics.jung.visualization.decorators.ToStringLabeller; +import edu.uci.ics.jung.visualization.picking.PickedState; +import edu.uci.ics.jung.visualization.renderers.Renderer; +import org.apache.commons.collections15.Transformer; +import org.w3c.dom.Document; +import javax.swing.*; +import javax.swing.border.EtchedBorder; +import java.awt.*; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.awt.geom.AffineTransform; +import java.awt.geom.Point2D; +import java.io.PrintWriter; +import java.util.*; + + +public class ContextAutomatonEditor extends JPanel implements RSObserver { + private enum EditorState {STATE, EDGE, DELETE, CLEAR, NONE} + + private static final long serialVersionUID = 1L; + + private ReactionSystem rs; + + //--------------------------------------------------------------- + // Visual configuration settings + //--------------------------------------------------------------- + private static final Color pickedNodeColor = Color.yellow; + //private static final Color pickedEdgeColor = Color.red; + private static final Color pickedEdgeColor = Color.black; + private static final Color edgeColor = Color.black; + private static final Color emptyEdgeColor = Color.lightGray; + private static final Font nodeLabelFont = new Font("Helvetica", Font.BOLD, 20); + private static final Font edgeLabelFont = new Font("Helvetica", Font.BOLD, 15); + private static final Font toolTipFont = new Font("Helvetica", Font.PLAIN, 14); + private static final float[] dash = {10.0f, 10.0f}; + private static final Stroke basicEdgeStroke = new BasicStroke(3.0f,BasicStroke.CAP_ROUND,BasicStroke.JOIN_ROUND); + private static final Stroke emptyEdgeStroke = new BasicStroke(3.0f, BasicStroke.CAP_ROUND, BasicStroke.JOIN_ROUND, 10.0f, dash, 0.f); + private static final Stroke basicEdgeArrow = new BasicStroke(3.0f); + private static final Stroke emptyEdgeArrow = new BasicStroke(3.0f, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND, 10.0f, dash, 10.0f); + + private static Dimension initialEditorSize; + + private VisualizationViewer graphViewer; + private Layout gLayout; + DefaultModalGraphMouse graphMouse; + private ContextAutomatonGraph graph; + + // Context menus for transitions, places and edges + private JPopupMenu stateContextMenu; + private JPopupMenu edgeContextMenu; + private TransitionEditor transitionEditor = null; + + private EditorState edtState; + private Vector modeButtons; + + private CAState lastPickedNode = null; + + + public ContextAutomatonEditor(Dimension size) { + this.setLayout(new BorderLayout()); + initialEditorSize = size; + + edtState = EditorState.NONE; + graph = new ContextAutomatonGraph(); + + createGraphEditor(); + createModeButtonsPanel(); + createContextMenus(); + + rs = ReactionSystem.getInstance(); + } + + public boolean isModified() { return graph.isModified(); } + + public void clearModificationStatus() { graph.clearModificationStatus(); } + + public String toRSSLString() { + return graph.toRSSLString(); + } + + public void exportToXML(PrintWriter output) { + updateNodesLocations(); + graph.exportToXML(output); + } + + public void loadFromXML(Document input) throws ContextAutomatonStructureError { + clear(); + graph.loadFromXML(input); + } + + + public void recalculateCoordinates() { + Layout autoLayout = new FRLayout(graph, graphViewer.getSize()); + autoLayout.initialize(); + + for (CAState state : graph.getVertices()) { + Point2D pos = autoLayout.transform(state); + state.updateLocation(pos); + } + } + + + public void clear() { + graph.clear(); + + for (EditorModeButton emb : modeButtons) + emb.setSelected(false); + + graphViewer.repaint(); + } + + public void lockNodesPositions(boolean lock) { + if (lock) + graphMouse.setMode(ModalGraphMouse.Mode.TRANSFORMING); + else + graphMouse.setMode(ModalGraphMouse.Mode.PICKING); + } + + public Set getReactantsSet() { return graph.getReactantsSet(); } + + //-------------------------------------------------------------------------- + // Creates visualization viewer for context automaton graph display/edition + //-------------------------------------------------------------------------- + private void createGraphEditor() { + gLayout = new StaticLayout(graph, + new Transformer() { + public Point2D transform(CAState node) { + return node.getLocation(); + } + }); + + graphViewer = new VisualizationViewer(gLayout, initialEditorSize) { + public JToolTip createToolTip() { + JToolTip tooltip = super.createToolTip(); + tooltip.setFont(toolTipFont); + return tooltip; + } + }; + + // Nodes labels + graphViewer.getRenderContext().setVertexLabelTransformer( + new ToStringLabeller()); + graphViewer.getRenderer().getVertexLabelRenderer() + .setPosition(Renderer.VertexLabel.Position.CNTR); + graphViewer.getRenderContext().setVertexFontTransformer( + new Transformer() { + public Font transform(CAState v) { + return nodeLabelFont; + } + }); + + // Nodes colour, background, etc. + graphViewer.getRenderContext().setVertexIconTransformer(new Transformer() { + public Icon transform(final CAState v) { + Color nodeColor = null; + + if(graphViewer.getPickedVertexState().isPicked(v)) + nodeColor = pickedNodeColor; + else + nodeColor = v.getFillColor(); + + return (v.isInitial() ? new SquareIcon(nodeColor, v.getWidth()) : new CircleIcon(nodeColor, v.getWidth())); + + }}); + + // Edge color, shape and weight + graphViewer.getRenderContext().setEdgeDrawPaintTransformer(new Transformer() { + public Paint transform(CAEdge e) { + return edgeColor; + } + }); + + graphViewer.getRenderContext().setEdgeStrokeTransformer(new Transformer() { + public Stroke transform(CAEdge e) { + return basicEdgeStroke; + } + }); + + graphViewer.getRenderContext().setEdgeArrowStrokeTransformer(new Transformer() { + public Stroke transform(CAEdge e) { + return basicEdgeArrow; + } + }); + + graphViewer.getRenderContext().setArrowFillPaintTransformer(new Transformer() { + public Paint transform(CAEdge caEdge) { + if (caEdge.hasTransition()) + return edgeColor; + else + return emptyEdgeColor; + } + }); + + graphViewer.getRenderContext().setEdgeShapeTransformer(new ConditionalEdgeShape<>(1.5f)); + + // Edge labels + graphViewer.getRenderContext().setEdgeLabelTransformer(new ToStringLabeller()); + graphViewer.getRenderContext().getEdgeLabelRenderer().setRotateEdgeLabels(true); + graphViewer.getRenderContext().setLabelOffset(20); + + graphViewer.getRenderContext().setEdgeFontTransformer(new Transformer() { + public Font transform(CAEdge CAEdge) { + return edgeLabelFont; + } + }); + + // For interactive graph editing + graphMouse = new DefaultModalGraphMouse(); + graphViewer.setGraphMouse(graphMouse); + + graphMouse.setMode(ModalGraphMouse.Mode.PICKING); + + graphViewer.setVertexToolTipTransformer(new Transformer() { + public String transform(CAState caState) { + return caState.getTooltipText(); + } + }); + + graphViewer.setEdgeToolTipTransformer(new Transformer() { + public String transform(CAEdge caEdge) { + return caEdge.getTooltipText(); + } + }); + + graphViewer.setBackground(Color.white); + graphViewer.setBorder(new EtchedBorder(EtchedBorder.LOWERED)); + graphViewer.addMouseListener(new EditorMouseListener()); + + add(graphViewer,BorderLayout.CENTER); + } + + //--------------------------------------------------------------- + // Create panel with buttons alowing editing mode choice + //--------------------------------------------------------------- + private void createModeButtonsPanel() { + modeButtons = new Vector(); + modeButtons.add(new EditorModeButton("STATE",new CircleIcon(CAState.baseFillColor, 15), EditorState.STATE, 0)); + modeButtons.add(new EditorModeButton("EDGE", EditorState.EDGE, 1)); + modeButtons.add(new EditorModeButton("DELETE", EditorState.DELETE, 2)); + modeButtons.add(new EditorModeButton("CLEAR", EditorState.CLEAR, 3)); + + ModeButtonsListener mbListener = new ModeButtonsListener(); + + for(int i=0;i pickedVertexState = graphViewer.getPickedVertexState(); + Set pickedNodes = pickedVertexState.getPicked(); + Iterator it = pickedNodes.iterator(); + + if(!it.hasNext()) { + return; + } + + CAState editedNode = it.next(); + pickedVertexState.clear(); + + graph.setInitialState(editedNode); + } + }); + + JMenuItem setLabelItem = new JMenuItem("Set label"); + setLabelItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + PickedState pickedVertexState = graphViewer.getPickedVertexState(); + Set pickedNodes = pickedVertexState.getPicked(); + Iterator it = pickedNodes.iterator(); + + if(!it.hasNext()) { + return; + } + + CAState state = it.next(); + pickedVertexState.clear(); + + showStateLabelEditDialog(state); + } + }); + + stateContextMenu.add(stateInitialItem); + stateContextMenu.add(setLabelItem); + stateContextMenu.setVisible(false); + + edgeContextMenu = new JPopupMenu(); + JMenuItem edgeLabelEditItem = new JMenuItem("Nondeterministic transitions"); + edgeLabelEditItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + PickedState pickedEdgeState = graphViewer.getPickedEdgeState(); + Set pickedEdges = pickedEdgeState.getPicked(); + Iterator it = pickedEdges.iterator(); + + if(!it.hasNext()) { + return; + } + + CAEdge editedEdge = it.next(); + pickedEdgeState.clear(); + showEdgeLabelEditDialog(editedEdge); + } + }); + + edgeContextMenu.add(edgeLabelEditItem); + edgeContextMenu.setVisible(false); + + transitionEditor = new TransitionEditor(); + } + + private void showStateLabelEditDialog(CAState state) { + String idRegex = "[a-zA-Z][a-zA-Z_0-9:-]*"; + boolean idOk = false; + + do { + String newLabel = JOptionPane.showInputDialog(this, "State label", state.getLabel()); + + if (newLabel == null) + return; + + newLabel = newLabel.trim(); + + if (!newLabel.matches(idRegex)) { + JOptionPane.showMessageDialog(this, + "State label should start with a letter and may contain only:
" + + "letters, numbers, colons (:), underscores (_) and hyphens (-)", + "Error", JOptionPane.ERROR_MESSAGE); + } + else { + idOk = true; + state.setLabel(newLabel); + } + } + while (!idOk); + + graph.markAsModified(); + this.repaint(); + } + + //--------------------------------------------------------------- + // Creates a simple dialog window for editing edge labels + //--------------------------------------------------------------- + private void showEdgeLabelEditDialog(CAEdge edge) { + Pair endPoints = graph.getEndpoints(edge); + transitionEditor.showTransitionEditDialog(this, edge.getTransitions(), endPoints.getFirst().getLabel(), endPoints.getSecond().getLabel()); + graph.markAsModified(); + graphViewer.repaint(); + rs.notifyObservers(); + } + + /** Updates coordinates stored in each graph node (eg. after interactive graph modification). + * Called before each storing net structure to the file. */ + private void updateNodesLocations() { + Collection nodes = graph.getVertices(); + + for(CAState n : nodes) { + n.updateLocation(gLayout.transform(n)); + } + } + + /** For better vertex placement */ + private void relax() { + Layout layout = graphViewer.getGraphLayout(); + layout.initialize(); + layout.setSize(graphViewer.getSize()); + Relaxer relaxer = graphViewer.getModel().getRelaxer(); + if (relaxer != null) { + relaxer.stop(); + relaxer.prerelax(); + relaxer.relax(); + } + } + + public void onRSUpdate() { + repaint(); + } + + //--------------------------------------------------------------------------------------------- + + + static class EditorModeButton extends JToggleButton { + private EditorState mode; + int seqNum; + + public EditorModeButton(String label, EditorState mode) { + super(label); + + this.mode = mode; + seqNum = 0; + } + + public EditorModeButton(String label, EditorState mode, int seqNum) { + super(label); + + this.mode = mode; + this.seqNum = seqNum; + } + + public EditorModeButton(String label, Icon icon, EditorState mode, int seqNum) { + super(label, icon); + + this.mode = mode; + this.seqNum = seqNum; + } + + public EditorState getMode() { + return mode; + } + + public int getSeqNum() { + return seqNum; + } + } + + + //--------------------------------------------------------------------------------------------- + + + class ModeButtonsListener implements ActionListener { + + public void actionPerformed(ActionEvent changeEvent) { + EditorModeButton emb = (EditorModeButton) changeEvent.getSource(); + + if(emb.isSelected()) { + int num = emb.getSeqNum(); + + for(int i=0;i pickSupport = null; + Layout layout = null; + CAState node = null; + CAEdge edge = null; + + switch(edtState) { + case STATE: + try { + // Transform screen coordinates to layout coordinates. + // Necessary for possible automaton structure viewer scaling. + Point2D nodeLocation = graphViewer.getRenderContext().getMultiLayerTransformer().inverseTransform(clickPt); + graph.addState(new CAState(nodeLocation)); + } catch (ContextAutomatonStructureError e) { + JOptionPane.showMessageDialog(null, + e.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + break; + + case EDGE: + PickedState pickedVertexState = graphViewer.getPickedVertexState(); + + pickSupport = graphViewer.getPickSupport(); + layout = graphViewer.getGraphLayout(); + node = pickSupport.getVertex(layout, clickPt.getX(), clickPt.getY()); + + if (node != null) { + if (lastPickedNode == null) { + lastPickedNode = node; + } else { + graph.addEdge(lastPickedNode, node); + lastPickedNode = null; + pickedVertexState.pick(node,false); + } + } else { + lastPickedNode = null; + } + + break; + + case DELETE: + pickSupport = graphViewer.getPickSupport(); + layout = graphViewer.getGraphLayout(); + node = pickSupport.getVertex(layout, clickPt.getX(), clickPt.getY()); + edge = pickSupport.getEdge(layout, clickPt.getX(), clickPt.getY()); + + if (node != null) { + Collection edges = graph.getIncidentEdges(node); + + for (CAEdge e : edges) + rs.removeCAEdge(e); + + graph.removeState(node); + } + else if (edge != null) { + graph.removeEdge(edge); + rs.removeCAEdge(edge); + } + + break; + + case NONE: + default: + break; + } + + me.consume(); + } + + private void rightButtonClicked(MouseEvent me) { + GraphElementAccessor pickSupport = graphViewer.getPickSupport(); + Layout layout = graphViewer.getGraphLayout(); + CAState node = pickSupport.getVertex(layout, me.getX(), me.getY()); + CAEdge edge = pickSupport.getEdge(layout, me.getX(), me.getY()); + + if (node != null) { + PickedState pickedVertexState = graphViewer.getPickedVertexState(); + pickedVertexState.clear(); + pickedVertexState.pick(node,true); + stateContextMenu.show(graphViewer, me.getX(), me.getY()); + } + else if (edge != null) { + PickedState pickedEdgeState = graphViewer.getPickedEdgeState(); + pickedEdgeState.clear(); + pickedEdgeState.pick(edge, true); + edgeContextMenu.show(graphViewer, me.getX(), me.getY()); + } + + me.consume(); + } + + }; + + //--------------------------------------------------------------------------------------------- + // For drawing the initial state + //--------------------------------------------------------------------------------------------- + + static class SquareIcon implements Icon { + private Color fillColor; + private int width; + + public SquareIcon(Color fColor, int width) { + fillColor = fColor; + this.width = width; + } + + public void paintIcon(Component c, Graphics g, int x, int y) { + g.setColor(fillColor); + g.fillRect(x, y, width, width); + g.setColor(Color.black); + g.drawRect(x, y, width, width); + } + + public int getIconWidth() { + return width; + } + + public int getIconHeight() { + return width; + } + } + + //--------------------------------------------------------------------------------------------- + // For drawing all non-initial states + //--------------------------------------------------------------------------------------------- + + static class CircleIcon implements Icon { + private Color fillColor; + private int radius; + + public CircleIcon(Color fColor, int radius) { + fillColor = fColor; + this.radius = radius; + } + + public void paintIcon(Component c, Graphics g, int x, int y) { + g.setColor(fillColor); + g.fillOval(x, y, radius, radius); + g.setColor(Color.black); + g.drawOval(x, y, radius, radius); + } + + public int getIconWidth() { + return radius; + } + + public int getIconHeight() { + return radius; + } + + } + +} + + +class ConditionalEdgeShape implements Transformer, E>, Shape> { + + private final EdgeShape.Loop loopShape; + private final Transformer, E>, Shape> defaultShape; + private final float loopScale; + + public ConditionalEdgeShape(float loopScale) { + this.loopShape = new EdgeShape.Loop<>(); + this.defaultShape = new EdgeShape.QuadCurve<>(); // or Line<> + this.loopScale = loopScale; + } + + public Shape transform(Context, E> context) { + Graph graph = context.graph; + E edge = context.element; + V src = graph.getSource(edge); + V dst = graph.getDest(edge); + + if (src.equals(dst)) { + // Scale the self-loop + Shape baseLoop = loopShape.transform(context); + + Rectangle bounds = baseLoop.getBounds(); + double centerX = bounds.getCenterX(); + double centerY = bounds.getCenterY(); + + AffineTransform at = new AffineTransform(); + at.translate(centerX, centerY); + at.scale(loopScale, loopScale); + at.translate(-centerX, -centerY); + + return at.createTransformedShape(baseLoop); + } else { + return defaultShape.transform(context); + } + } +} diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java new file mode 100644 index 0000000..ffd3305 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ContextAutomatonGraph.java @@ -0,0 +1,438 @@ +package pl.umk.mat.martinp.reactics; + + +import edu.uci.ics.jung.graph.DirectedSparseGraph; +import edu.uci.ics.jung.graph.util.Pair; +import org.w3c.dom.Document; +import org.w3c.dom.Element; +import org.w3c.dom.Node; +import org.w3c.dom.NodeList; +import java.awt.*; +import java.awt.geom.Point2D; +import java.io.PrintWriter; +import java.util.*; + + +class ContextAutomatonGraph extends DirectedSparseGraph { + private static final long serialVersionUID = 1L; + + HashMap states = new HashMap<>(); + private CAState initialState = null; + boolean modified = false; + + public ContextAutomatonGraph() { + super(); + } + + public boolean isModified() { return modified; } + + public void markAsModified() { modified = true; } + + public void clearModificationStatus() { modified = false; } + + String toRSSLString() { + StringBuilder rsslString = new StringBuilder("context-automaton {\n"); + + rsslString.append(" states { "); + Collection allStates = states.values(); + Iterator it = allStates.iterator(); + if (it.hasNext()) { + rsslString.append(it.next().getLabel()); + } + while (it.hasNext()) { + rsslString.append(", ").append(it.next().getLabel()); + } + rsslString.append(" };\n"); + + rsslString.append(" init-state { ").append(initialState != null ? initialState.getLabel() : "").append(" };\n"); + rsslString.append(" transitions {\n"); + + for (CAEdge edge : this.getEdges()) { + for (Transition tr : edge.getTransitions()) { + rsslString.append(" { ").append(tr.context).append(" }: "); + rsslString.append(this.getSource(edge).label).append(" -> ").append(this.getDest(edge).label); + + String guard = tr.guard; + + if (guard.length() > 0) { + rsslString.append(" : ").append(guard); + } + + rsslString.append(";\n"); + } + } + rsslString.append(" };\n"); + + rsslString.append("};\n"); + + return rsslString.toString(); + } + + public void exportToXML(PrintWriter output) { + output.println(" "); + + for (CAState state : states.values()) { + Point2D pos = state.getLocation(); + output.print(" "); + } + + for (CAEdge edge : edges.keySet()) { + Pair endPts = this.getEndpoints(edge); + output.print(" "); + + for (Transition tr : edge.getTransitions()) { + output.print(" "); + } + output.println(" "); + } + + output.println(" "); + } + + /** + * Reads the context automaton structure from the XML file. + * + * @param input An XML file containing a valid description of a context automaton. + * @throws ContextAutomatonStructureError In the case of inputFile structure error, eg. \ + * more than one context-automaton section, more than one \ + * initial state, repeating state identifiers, \ + * edge between non-existing nodes, etc. + */ + public void loadFromXML(Document input) throws ContextAutomatonStructureError { + NodeList caSections = input.getElementsByTagName("context-automaton"); + + if (caSections.getLength() == 0 || caSections.getLength() > 1) { + throw new ContextAutomatonStructureError("An XML file should contain a single context automaton description."); + } + + //-------------------------------------------------------------------------------------------------------------- + // Retrieve the states + //-------------------------------------------------------------------------------------------------------------- + + HashMap states = new HashMap(); + NodeList stateList = input.getElementsByTagName("state"); + boolean hasInitialState = false; + + for (int idx = 0; idx < stateList.getLength(); ++idx) { + Node stateNode = stateList.item(idx); + + if (stateNode.getNodeType() != Node.ELEMENT_NODE) { + continue; + } + + Element stateElement = (Element) stateNode; + + int id = Integer.parseInt(stateElement.getAttribute("id")); + double x = Double.parseDouble(stateElement.getAttribute("x")); + double y = Double.parseDouble(stateElement.getAttribute("y")); + String name = stateElement.getAttribute("name"); + String initial = stateElement.getAttribute("initial"); + + if (states.containsKey(name)) { + throw new ContextAutomatonStructureError("State name <" + name + "> already used."); + } + + CAState newState = new CAState(id, name, new Point2D.Double(x, y)); + this.addState(newState); + states.put(name, newState); + + if (initial.equals("true")) { + if (hasInitialState) + throw new ContextAutomatonStructureError("There should not be more than one initial state."); + + hasInitialState = true; + this.setInitialState(newState); + } + } + + //-------------------------------------------------------------------------------------------------------------- + // Retrieve the edges + //-------------------------------------------------------------------------------------------------------------- + + NodeList edgeList = input.getElementsByTagName("edge"); + + for (int idx = 0; idx < edgeList.getLength(); ++idx) { + Node edgeNode = edgeList.item(idx); + + if (edgeNode.getNodeType() != Node.ELEMENT_NODE) { + continue; + } + + Element edgeElement = (Element) edgeNode; + + String from = edgeElement.getAttribute("from"); + String to = edgeElement.getAttribute("to"); + + // Retrieve all child nodes describing nondeterministic transitions related to this edge + NodeList childNodeList = edgeNode.getChildNodes(); + Vector transitionList = new Vector(); + + for (int cIdx=0; cIdx < childNodeList.getLength(); ++ cIdx) { + Node childNode = childNodeList.item(cIdx); + + if (childNode.getNodeType() != Node.ELEMENT_NODE) { + continue; + } + + Element transElement = (Element) childNode; + transitionList.add(new Transition(transElement.getAttribute("context"), transElement.getAttribute("guard"))); + } + + CAState stateFrom = states.get(from); + CAState stateTo = states.get(to); + + if (stateFrom == null || stateTo == null) + throw new ContextAutomatonStructureError("An edge may be created only between existing nodes."); + + this.addEdge(stateFrom, stateTo, transitionList); + } + } + + public Set getReactantsSet() { + Set reactants = new HashSet(); + + for (CAEdge edge : getEdges()) { + for (Transition trans : edge.getTransitions()) { + int start = trans.context.indexOf("{"); + int end = trans.context.indexOf("}"); + + if (start != -1 && end != -1 && start < end) { + reactants.addAll(Arrays.asList(trans.context.substring(start + 1, end).split("\\s*,\\s*"))); + } + } + } + + return reactants; + } + + public void setInitialState(CAState state) { + if (initialState != null) + initialState.setInitial(false); + + state.setInitial(true); + initialState = state; + modified = true; + } + + public CAState getInitialState() { + return initialState; + } + + /** + * Clears the entire automaton structure structure + */ + public void clear() { + for (CAState st : states.values()) + removeVertex(st); + + states.clear(); + CAState.resetIdCounter(); + modified = true; + } + + public boolean addEdge(CAState from, CAState to) { + modified = true; + + return this.addEdge(new CAEdge(), from, to); + } + + public void addEdge(CAState from, CAState to, Collection transitionList) { + CAEdge edge = this.findEdge(from, to); + + if (edge == null) { + CAEdge caEdge = ReactionSystem.getInstance().createCAEdge(); + caEdge.addTransitions(transitionList); + this.addEdge(caEdge, from, to); + } + else + edge.addTransitions(transitionList); + + modified = true; + } + + public void addState(CAState state) throws ContextAutomatonStructureError { + int stateId = state.getId(); + + if (states.get(stateId) != null) + throw new ContextAutomatonStructureError("State id " + stateId + " already in use."); + + states.put(stateId, state); + this.addVertex(state); + modified = true; + } + + public boolean removeState(CAState state) { + if (states.get(state.getId()) != null) { + states.remove(state.getId()); + } + + modified = true; + + // Remove the state with all connected edges + return this.removeVertex(state); + } + +} + + +//------------------------------------------------------------------------------------------------- +// Single node of the context automaton graph +//------------------------------------------------------------------------------------------------- + +class CAState { + public final static Color baseFillColor = Color.lightGray; + public final static Color selectedFillColor = Color.lightGray; + public final static Color initStateFillColor = new Color(102, 178, 255); + + private static final int nodeWidth = 30; + private static final int nodeHeight = 30; + protected static int nextId = 1; + + /** Unique auto incremented identifier of the node */ + protected int id; + + /** User defined label of the node displayed as a tool tip and used in RSSL and XML files */ + protected String label; + + protected Point2D location; + private boolean isInitial = false; + + /** A state created from the description stored in a file. */ + public CAState(int id, String label, Point2D location) { + this.id = id; + this.label = label; + this.location = location; + + // To avoid duplicate node identifiers + if (id >= nextId) + nextId = id + 1; + } + + /** A state created by clicking in graphical component. */ + public CAState(Point2D location) { + this.id = nextId; + this.label = "q" + id; + this.location = location; + ++nextId; + } + + public Point2D getLocation() { return location; } + public void updateLocation(Point2D location) { this.location = location; } + + public boolean isInitial() { return isInitial; } + public void setInitial(boolean status) { isInitial = status; } + + public int getWidth() { return nodeWidth; } + public int getHeight() { return nodeHeight; } + + public String getLabel() { return label; } + public void setLabel(String newLabel) { label = newLabel; } + + public int getId() { return id; } + + static void resetIdCounter() { nextId = 1; } + + public String toString() { return Integer.toString(id); } + + public String getTooltipText() { + return ""+ + "State " + id + "
" + getLabel() + //"
"+ + ""; + } + + Color getFillColor() { + return isInitial ? initStateFillColor : baseFillColor; + } +} + + +//------------------------------------------------------------------------------------------------- +// Single edge of the context automaton graph. +// Each edge can represent a number of single transitions between the same pair of automaton states. +//------------------------------------------------------------------------------------------------- + +class CAEdge { + protected static int nextId = 0; + + protected int id; + + // The list of all nondeterministic transitions represented by this edge + private Vector transitions = new Vector(); + + public boolean hasTransition() { return transitions.size() > 0; } + + + public CAEdge() { + this.id = nextId++; + } + +// public CAEdge(Collection transitionList) { +// this.transitions.addAll(transitionList); +// } + + Vector getTransitions() { + return transitions; + } + + public int getId() { + return id; + } + + public String toString() { + // Update this if you need any label displayed together with graph edge + return ""; + } + + public String getTooltipText() { + StringBuilder tooTip = new StringBuilder("
Context : Guard
"); + + for (Transition tr : transitions) { + tooTip.append(tr.context).append(" : ").append(tr.guard).append("
"); + } + + tooTip.append(""); + + return tooTip.toString(); + } + + public void addTransitions(Collection transitionList) { + transitions.addAll(transitionList); + } +} + + +//------------------------------------------------------------------------------------------------- +// Single transition. To be included in a multiedge. +//------------------------------------------------------------------------------------------------- + +class Transition { + String context; + String guard; + + public Transition(String ctx, String grd) { + context = ctx; + guard = grd; + } +} + + +class ContextAutomatonStructureError extends FileStructureError { + public ContextAutomatonStructureError(String message) { + super(message); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java new file mode 100644 index 0000000..0b32f30 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/CumulatedReactionsViewer.java @@ -0,0 +1,13 @@ +package pl.umk.mat.martinp.reactics; + +import javax.swing.*; +import java.awt.*; + +public class CumulatedReactionsViewer extends JPanel { + + public CumulatedReactionsViewer() { + this.setLayout(new BorderLayout()); + this.add(new JLabel("Cumulate Reactions Viewer", SwingConstants.CENTER), BorderLayout.CENTER); + } + +} diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java new file mode 100644 index 0000000..9ce60e6 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/FormulaEditor.java @@ -0,0 +1,410 @@ +package pl.umk.mat.martinp.reactics; + +import org.w3c.dom.Document; +import org.w3c.dom.Element; +import org.w3c.dom.Node; +import org.w3c.dom.NodeList; + +import javax.swing.*; +import javax.swing.border.Border; +import javax.swing.border.EtchedBorder; +import javax.swing.event.TableModelEvent; +import javax.swing.event.TableModelListener; +import javax.swing.table.*; +import java.awt.*; +import java.io.*; +import java.util.Collection; +import java.util.Vector; + + +public class FormulaEditor extends JPanel implements RSObserver { + private FormulaTableModel ftModel; + private JTable formTable; + private ReactionSystem rs; + private Vector formulaList; + + boolean modified = false; + + static final Color TableHeaderBackgroundColor = Color.gray; + static final Color TableHeaderFontColor = Color.white; + static final Color BaseFormulaBackgroundColor = Color.white; + static final Color TrueFormulaBackgroundColor = new Color(138, 242, 183); + static final Color FalseFormulaBackgroundColor = new Color(240, 141, 141); + static final Color InvalidFormulaBackgroundColor = new Color(124, 124, 124); + static final Border emptyBorder = BorderFactory.createEmptyBorder(1, 1, 1, 1); + static final Border selectedBorder = BorderFactory.createLineBorder(Color.RED, 2); + + + public FormulaEditor(ReactionSystem rs) { + this.rs = rs; + formulaList = rs.formulas; + + // Create the table for displaying formulas. Prevent default selection modes. + ftModel = new FormulaTableModel(); + formTable = new JTable(ftModel, new FormulaColumnModel()); + formTable.setCellSelectionEnabled(false); + formTable.setRowSelectionAllowed(true); + + Font headerFont = formTable.getTableHeader().getFont(); + Font cellFont = formTable.getFont(); + JTableHeader formHeader = formTable.getTableHeader(); + formTable.setFont(new Font("Monospaced", Font.PLAIN, cellFont.getSize() + 2)); + formHeader.setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2)); + formHeader.setBackground(TableHeaderBackgroundColor); + formHeader.setForeground(TableHeaderFontColor); + formHeader.setReorderingAllowed(false); + formHeader.setResizingAllowed(true); + formHeader.setBorder(new EtchedBorder(EtchedBorder.LOWERED)); + + FormulaTableCellRenderer renderer = new FormulaTableCellRenderer(); + formTable.setDefaultRenderer(Object.class, renderer); + formTable.createDefaultColumnsFromModel(); + + setLayout(new BorderLayout()); + add(new JScrollPane(formTable), BorderLayout.CENTER); + } + + public boolean isModified() { return modified; } + + public void clearModificationStatus() { modified = false; } + + public String toRSSLString() { + StringBuilder rsslString = new StringBuilder(); + + for (Formula f: formulaList) + rsslString.append(f.toRSSLString()).append("\n"); + + return rsslString.toString(); + } + + public void exportToXML(PrintWriter output) { + output.println(" "); + + for (Formula f : formulaList) + output.println(" " + f.toXMLString()); + + output.println(" "); + } + + public void loadFromXML(Document input) { + formulaList.clear(); + + NodeList formulaTags = input.getElementsByTagName("formula"); + + for (int idx = 0; idx < formulaTags.getLength(); ++idx) { + Node formulaNode = formulaTags.item(idx); + + if (formulaNode.getNodeType() != Node.ELEMENT_NODE) { + continue; + } + + Element formulaElement = (Element) formulaNode; + + String label = formulaElement.getAttribute("label"); + String formula = formulaElement.getTextContent(); + formulaList.add(new Formula(label, formula)); + } + + ftModel.fireTableDataChanged(); + } + + private boolean showFormulaEditDialog(JFrame parent, Formula ff) { + final int Select = 0; + final int Approve = 1; + + JTextField labelInput = new JTextField(30); + JTextField formulaInput = new JTextField(30); + + String labelStr = ""; + String formulaStr = ""; + + labelStr = ff.label; + formulaStr = ff.formula; + + labelInput.setToolTipText("A unique label of the formula"); + formulaInput.setToolTipText("Formula to be evaluated"); + + JPanel myPanel = new JPanel(new GridBagLayout()); + GridBagConstraints cs = new GridBagConstraints(); + + cs.insets = new Insets(5, 5, 5, 5); + cs.anchor = GridBagConstraints.WEST; + cs.gridx = 0; + cs.gridy = 0; + myPanel.add(new JLabel("Label"), cs); + + cs.gridx = 1; + cs.gridy = 0; + myPanel.add(labelInput, cs); + + cs.gridx = 0; + cs.gridy = 1; + myPanel.add(new JLabel("Formula"), cs); + + cs.gridx = 1; + cs.gridy = 1; + myPanel.add(formulaInput, cs); + + int opStatus = Select; + + do { + labelInput.setText(labelStr); + formulaInput.setText(formulaStr); + + int result = JOptionPane.showConfirmDialog(parent, myPanel, + "Formula details", JOptionPane.OK_CANCEL_OPTION); + + if (result != JOptionPane.OK_OPTION) { + return false; + } + + labelStr = labelInput.getText(); + formulaStr = formulaInput.getText(); + + ff.label = labelStr; + ff.formula = formulaStr; + + opStatus = Approve; + } + while(opStatus == Select); + + return true; + } + + public void addFormula(JFrame parent) { + Formula ff = new Formula(); + + if (showFormulaEditDialog(parent, ff)) { + formulaList.add(ff); + modified = true; + ftModel.fireTableDataChanged(); + } + } + + // If more than one formula is selected throw an exception only the first can be edited + public void editFormula(JFrame parent) { + int[] selected = formTable.getSelectedRows(); + + if (selected.length != 1) { + JOptionPane.showMessageDialog(parent, "Select a single formula to edit.", "Select formula", JOptionPane.WARNING_MESSAGE); + return; + } + + Formula fEdt = formulaList.get(formTable.convertRowIndexToModel(selected[0])); + + if (fEdt == null) + return; + + showFormulaEditDialog(parent, fEdt); + fEdt.status = Formula.FormulaStatus.None; + modified = true; + ftModel.fireTableDataChanged(); + } + + public void removeFormulas() { + int[] viewRows = formTable.getSelectedRows(); + + // Remove formulas starting from the last to avoid indexes updates + for (int vIdx = viewRows.length - 1; vIdx>=0; --vIdx) { + int mr = formTable.convertRowIndexToModel(viewRows[vIdx]); + formulaList.remove(mr); + } + + modified = true; + ftModel.fireTableDataChanged(); + } + + public Collection getSelectedFormulas() { + Vector selected = new Vector(); + int[] viewRows = formTable.getSelectedRows(); + + for (int vr : viewRows) { + int mr = formTable.convertRowIndexToModel(vr); + selected.add(formulaList.get(mr)); + } + + return selected; + } + + // Needed to repaint JTable. Called after content modification by an external object. + public void refreshStatus() { + ftModel.fireTableDataChanged(); + } + + public void resetFormulasStatus() { + for (Formula ff : formulaList) { + ff.status = Formula.FormulaStatus.None; + ff.mcTime = ff.totalTime = ff.memory = "-"; + } + + ftModel.fireTableDataChanged(); + } + + public void onRSUpdate() { + resetFormulasStatus(); + refreshStatus(); + } + + static class FormulaColumnModel extends DefaultTableColumnModel { + int colno = 0; + + public void addColumn(TableColumn tc) { + switch (colno) { + case 0 -> { + tc.setMinWidth(60); + tc.setMaxWidth(Integer.MAX_VALUE / 10); + tc.setPreferredWidth(100); + } + case 1 -> { + tc.setMinWidth(100); + tc.setMaxWidth(Integer.MAX_VALUE); + } + case 2, 3, 4, 5 -> { + tc.setMinWidth(50); + tc.setPreferredWidth(50); + tc.setMaxWidth(Integer.MAX_VALUE / 10); + } + } + + super.addColumn(tc); + ++colno; + } + } + + + class FormulaTableModel extends AbstractTableModel implements TableModelListener { + private final String[] columnNames = {"Label", "Formula", "Status", "MC Time (s)", "Total Time (s)", "Memory (MB)"}; + + public String getColumnName(int colIdx) { + return columnNames[colIdx]; + } + + public int getRowCount() { + return formulaList.size(); + } + + public int getColumnCount() { + return columnNames.length; + } + + public Object getValueAt(int row, int column) { + Formula ff = formulaList.get(row); + + return switch (column) { + case 0 -> ff.label; + case 1 -> ff.formula; + case 2 -> ff.status; + case 3 -> ff.mcTime; + case 4 -> ff.totalTime; + case 5 -> ff.memory; + default -> ""; + }; + } + + public void setValueAt(Object value, int row, int column) { +// fireTableDataChanged(); + } + + public boolean isCellEditable(int rowIndex, int columnIndex) { return false; } + + public Class getColumnClass(int column) { + return getValueAt(0, column).getClass(); + } + + public void tableChanged(TableModelEvent tableModelEvent) { } + } + + + // To properly display the content of the table containing formulas + class FormulaTableCellRenderer extends JLabel implements TableCellRenderer { + + public FormulaTableCellRenderer() { + // Allows background to be visible + setOpaque(true); + } + + public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) { + String statusStr = ""; + Formula ff = formulaList.get(row); + + setForeground(Color.black); + + if (isSelected) { + setBorder(selectedBorder); + } + else { + setBorder(emptyBorder); + } + + // Set cell background and formula evaluation status + if (column == 2) { + switch (ff.status) { + case None -> { + statusStr = "?"; + setBackground(BaseFormulaBackgroundColor); + } + case True -> { + statusStr = "True"; + setBackground(TrueFormulaBackgroundColor); + } + case False -> { + statusStr = "False"; + setBackground(FalseFormulaBackgroundColor); + } + case Invalid -> { + statusStr = "Invalid"; + setBackground(InvalidFormulaBackgroundColor); + } + } + + setText(statusStr); + } + else { + setText((String) value); + setBackground(BaseFormulaBackgroundColor); + } + + if (column > 2) { + setHorizontalAlignment(SwingConstants.RIGHT); + } else { + setHorizontalAlignment(SwingConstants.LEFT); + } + + return this; + } + } +} + + +class Formula { + public enum FormulaStatus {None, True, False, Invalid}; + + String label; + String formula; + FormulaStatus status; + String mcTime; + String totalTime; + String memory; + + public Formula() { + this("", ""); + } + + public Formula(String label, String formula) { + this.label = label; + this.formula = formula; + this.status = FormulaStatus.None; + this.mcTime = this.totalTime = this.memory = "-"; + } + + public String toRSSLString() { + return "rsctlk-property { " + label + " : " + formula + " };"; + } + + public String toXMLString() { + return "" + + formula.replaceAll("<", "<").replaceAll(">", ">") + + ""; + } +} + diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java new file mode 100644 index 0000000..9e970cf --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/HelpWindow.java @@ -0,0 +1,125 @@ +package pl.umk.mat.martinp.reactics; + +import javax.swing.*; +import javax.swing.border.*; +import javax.swing.event.*; +import java.awt.*; +import java.awt.event.*; +import java.net.*; + +public class HelpWindow extends JFrame { + private static final long serialVersionUID = 327019113533268901L; + private static final String startDocument = "index.html"; + private static final String docPath = "/help/"; + + private static HelpWindow instance = null; + private static JTextPane helpPane = new JTextPane();; + + public static synchronized HelpWindow getInstance() { + if (instance == null) + instance = new HelpWindow(); + + return instance; + } + + private HelpWindow() { + super("ReactICS GUI Help"); + + getContentPane().setLayout(new BorderLayout()); + + JPanel mainPanel = new JPanel(); + mainPanel.setLayout(new BorderLayout()); + EtchedBorder panelBorder = new EtchedBorder(EtchedBorder.LOWERED); + mainPanel.setBorder(panelBorder); + + helpPane.setEditable(false); + helpPane.addHyperlinkListener(new HyperlinkListener() { + public void hyperlinkUpdate(HyperlinkEvent hle) { + if (hle.getEventType() == HyperlinkEvent.EventType.ACTIVATED) { + String target = hle.getDescription(); + + if (target.startsWith("#")) { + helpPane.scrollToReference(target.substring(1)); + } + } + } + }); + + try { + URL helpUrl = this.getClass().getResource(docPath + startDocument); + helpPane.setPage(helpUrl); + + helpPane.revalidate(); + helpPane.repaint(); + } + catch (Exception e) { + System.out.println("Exception: " + e.getMessage()); + JOptionPane.showMessageDialog(null, "Can not load help content", + "Help", JOptionPane.ERROR_MESSAGE); + } + + JScrollPane helpScroller = new JScrollPane(); + JViewport helpVp = new JViewport(); + Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); + helpVp.setPreferredSize(new Dimension(screenSize.width/2, screenSize.height-200)); + helpVp.add(helpPane); + helpScroller.setViewport(helpVp); + mainPanel.add(helpScroller, BorderLayout.CENTER); + getContentPane().add(mainPanel, BorderLayout.CENTER); + + pack(); + } + + public void show(Component parent) { + setLocationRelativeTo(parent); + setVisible(true); + } + +} + + +class AboutWindow extends JFrame { + private static AboutWindow instance = null; + + public static synchronized AboutWindow getInstance() { + if (instance == null) + instance = new AboutWindow(); + + return instance; + } + + private AboutWindow() { + super("About ..."); + + getContentPane().setLayout(new BorderLayout()); + + JPanel infoPanel = new JPanel(); + infoPanel.add(new JLabel("

" + ReacticsGUI.ApplicationName + "

" + + "

version " + ReacticsGUI.ApplicationVersion + " (" + ReacticsGUI.ApplicationReleaseDate + ")

" + + "

Model Checker for Reaction Systems

" + + "

ReactICS Research Team (CC BY 4.0)

" + + "

https://reactics.org

")); + getContentPane().add(infoPanel, BorderLayout.CENTER); + + JButton closeButton = new JButton("Close"); + closeButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + setVisible(false); + } + }); + JPanel ctrlPanel = new JPanel(); + ctrlPanel.add(closeButton); + ctrlPanel.setAlignmentX(SwingConstants.RIGHT); + getContentPane().add(ctrlPanel, BorderLayout.SOUTH); + + setSize(new Dimension(400, 250)); + setResizable(false); + this.setAlwaysOnTop(true); + this.setUndecorated(true); + } + + public void show(Component parent) { + setLocationRelativeTo(parent); + setVisible(true); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java new file mode 100644 index 0000000..8ace501 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ProcessEditor.java @@ -0,0 +1,427 @@ +package pl.umk.mat.martinp.reactics; + +import javax.swing.*; +import javax.swing.border.*; +import javax.swing.table.AbstractTableModel; +import java.awt.*; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.io.PrintWriter; +import java.util.*; + + +//------------------------------------------------------------------------------------------------- +// Graphical component for editing a single process (list of reactions) +//------------------------------------------------------------------------------------------------- + +class ProcessEditor extends JPanel { + private JTable reactionList; + private RSTableModel reactionsModel; + + private RSProcess rsProcess; + private boolean modified = false; + + private JCheckBox selectBox; + private TitledBorder outBorder; + private ReactionSystem rs; + + private final Color borderColor = new Color(24, 104, 92);; + private final Color selectedBorderColor = new Color(150, 10, 10); + private static final int borderThickness = 4; + + public ProcessEditor(RSProcess rsProc) { + rsProcess = rsProc; + init(); + } + + public RSProcess getProcess() { return rsProcess; } + + public boolean isSelected() { + return selectBox.isSelected(); + } + + public boolean isModified() { return modified; } + + public void clearModificationStatus() { modified = false; } + + public String getLabel() { + return rsProcess.label; + } + + private void init() { + // Create border for the component + outBorder = BorderFactory.createTitledBorder(rsProcess.label); + Font font = outBorder.getTitleFont(); + Font newFont = new Font (font.getFamily(), Font.BOLD, font.getSize() + 2); + outBorder.setTitleFont(new Font (font.getFamily(), Font.BOLD, font.getSize() + 2)); + outBorder.setTitleColor(borderColor); + outBorder.setBorder(new LineBorder(borderColor, borderThickness, true)); + setBorder(outBorder); + + // Create reactions list component + reactionsModel = new RSTableModel(); + reactionList = new JTable(reactionsModel); + + Font cellFont = reactionList.getFont(); + Font headerFont = reactionList.getTableHeader().getFont(); + + reactionList.setFont(new Font("Monospaced", 0, cellFont.getSize() + 2)); + reactionList.getTableHeader().setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2)); + reactionList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); + + setLayout(new BoxLayout(this, BoxLayout.Y_AXIS)); + + JPanel buttonPanel = new JPanel(); + + JButton addButton = new JButton("Add reaction"); + addButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { addReaction(); } + }); + buttonPanel.add(addButton); + + JButton edtButton = new JButton("Edit reaction"); + edtButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + editReaction(); + } + }); + buttonPanel.add(edtButton); + + JButton rmButton = new JButton("Remove reaction"); + rmButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + removeReactions(); + } + }); + buttonPanel.add(rmButton); + + selectBox = new JCheckBox("Select"); + selectBox.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + toggleSelection(); + } + }); + buttonPanel.add(selectBox); + + add(buttonPanel); + + add(new JScrollPane(reactionList)); + + setPreferredSize(new Dimension(-1, 200)); + + rs = ReactionSystem.getInstance(); + } + + private boolean showReactionEditDialog(JComponent parent, Reaction rr) { + final int Select = 0; + final int Approve = 1; + + JTextField reactantsInput = new JTextField(30); + JTextField inhibitorsInput = new JTextField(30); + JTextField productsInput = new JTextField(30); + + String reactantsStr = ""; + String inhibitorsStr = ""; + String productsStr = ""; + + Iterator it = rr.reactants.iterator(); + StringBuilder dataStr = new StringBuilder(); + + while (it.hasNext()) + dataStr.append(it.next()).append(" "); + + reactantsStr = dataStr.toString(); + + it = rr.inhibitors.iterator(); + dataStr.setLength(0); + + while (it.hasNext()) + dataStr.append(it.next()).append(" "); + + inhibitorsStr = dataStr.toString(); + + it = rr.products.iterator(); + dataStr.setLength(0); + + while (it.hasNext()) + dataStr.append(it.next()).append(" "); + + productsStr = dataStr.toString(); + + reactantsInput.setToolTipText("Space separated list of reactants"); + inhibitorsInput.setToolTipText("Space separated list of inhibitors"); + productsInput.setToolTipText("Space separated list of products"); + + JPanel myPanel = new JPanel(new GridBagLayout()); + GridBagConstraints cs = new GridBagConstraints(); + + cs.insets = new Insets(5, 5, 5, 5); + cs.anchor = GridBagConstraints.WEST; + cs.gridx = 0; + cs.gridy = 0; + myPanel.add(new JLabel("Reactants"), cs); + + cs.gridx = 1; + cs.gridy = 0; + myPanel.add(reactantsInput, cs); + + cs.gridx = 0; + cs.gridy = 1; + myPanel.add(new JLabel("Inhibitors"), cs); + + cs.gridx = 1; + cs.gridy = 1; + myPanel.add(inhibitorsInput, cs); + + cs.gridx = 0; + cs.gridy = 2; + myPanel.add(new JLabel("Products"), cs); + + cs.gridx = 1; + cs.gridy = 2; + myPanel.add(productsInput, cs); + + int opStatus = Select; + + do { + reactantsInput.setText(reactantsStr); + inhibitorsInput.setText(inhibitorsStr); + productsInput.setText(productsStr); + + int result = JOptionPane.showConfirmDialog(parent, myPanel, + "Reaction details", JOptionPane.OK_CANCEL_OPTION); + + if (result != JOptionPane.OK_OPTION) { + return false; + } + + reactantsStr = reactantsInput.getText(); + inhibitorsStr = inhibitorsInput.getText(); + productsStr = productsInput.getText(); + + HashSet reactantsSet = new HashSet(Arrays.asList(reactantsStr.trim().split("\\s+"))); + HashSet inhibitorsSet = new HashSet(Arrays.asList(inhibitorsStr.trim().split("\\s+"))); + HashSet productsSet = new HashSet(Arrays.asList(productsStr.trim().split("\\s+"))); + + // Verify that reactant and inhibitor sets have empty intersection + boolean intersection = false; + + for (String entity : inhibitorsSet) { + if (reactantsSet.contains(entity)) { + intersection = true; + break; + } + } + + if (intersection) { + JOptionPane.showMessageDialog(this, "Reactant and inhibitor sets have to be disjoint.", "Error", JOptionPane.ERROR_MESSAGE); + continue; + } + + rr.reactants.clear(); + rr.reactants.addAll(reactantsSet); + rr.inhibitors.clear(); + rr.inhibitors.addAll(inhibitorsSet); + rr.products.clear(); + rr.products.addAll(productsSet); + + opStatus = Approve; + } + while(opStatus == Select); + + return true; + } + + public Set getReactantsSet() { + HashSet rset = new HashSet(); + + for (Reaction rr : rsProcess.reactions) + rset.addAll(rr.getReactantsSet()); + + return rset; + } + + public void exportToXML(PrintWriter output) { + output.println(" "); + + for (Reaction rr : rsProcess.reactions) + rr.exportToXML(output); + + output.println(" "); + } + + public String toRSSLString() { + StringBuilder rsslString = new StringBuilder(" " + rsProcess.label + " {\n"); + + for (Reaction rr : rsProcess.reactions) { + rsslString.append(rr.toRSSLString()); + } + + rsslString.append(" };\n"); + + return rsslString.toString(); + } + + void rename(String newLabel) { + rsProcess.label = newLabel; + outBorder.setTitle(rsProcess.label); + + this.repaint(); + } + + // Add new reaction + public void addReaction(Reaction rr) { + rsProcess.reactions.add(rr); + reactionsModel.fireTableDataChanged(); + } + + private void addReaction() { + Reaction rr = new Reaction(); + if (!showReactionEditDialog(this, rr)) + return; + + rsProcess.reactions.add(rr); + modified = true; + reactionsModel.fireTableDataChanged(); + rs.notifyObservers(); + } + + // Edit details of an existing reaction + private void editReaction() { + int rIdx = reactionList.getSelectedRow(); + + if (rIdx == -1) { + JOptionPane.showMessageDialog(this, "Select the reaction to edit.", "Select reaction", JOptionPane.WARNING_MESSAGE); + return; + } + + Reaction rr = new Reaction(rsProcess.reactions.get(rIdx)); + reactionList.clearSelection(); + if (!showReactionEditDialog(this, rr)) { + return; + } + + rsProcess.reactions.setElementAt(rr, rIdx); + modified = true; + reactionsModel.fireTableDataChanged(); + rs.notifyObservers(); + } + + // Remove an existing reaction + private void removeReactions() { + int rIdx = reactionList.getSelectedRow(); + + if (rIdx == -1) { + JOptionPane.showMessageDialog(this, "Select the reaction to be removed.", "Select reaction", JOptionPane.WARNING_MESSAGE); + return; + } + + rsProcess.reactions.remove(rIdx); + reactionList.clearSelection(); + reactionsModel.fireTableDataChanged(); + modified = true; + this.repaint(); + rs.notifyObservers(); + } + + private void toggleSelection() { + if (selectBox.isSelected()) { + outBorder.setTitleColor(selectedBorderColor); + outBorder.setBorder(new LineBorder(selectedBorderColor, borderThickness, true)); + } + else { + outBorder.setTitleColor(borderColor); + outBorder.setBorder(new LineBorder(borderColor, borderThickness, true)); + } + + this.repaint(); + } + + class RSTableModel extends AbstractTableModel { + + private String columnNames[] = {"Reactants", "Inhibitors", "Results"}; + private Vector[] data; + + public String getColumnName(int colIdx) { + return columnNames[colIdx]; + } + + public int getRowCount() { + return rsProcess.reactions.size(); + } + + public int getColumnCount() { + return columnNames.length; + } + + public Object getValueAt(int row, int column) { + Reaction rr = rsProcess.reactions.get(row); + + return switch (column) { + case 0 -> rr.reactants; + case 1 -> rr.inhibitors; + case 2 -> rr.products; + default -> ""; + }; + } + + public boolean isCellEditable(int rowIndex, int columnIndex) { + return false; + } + } + +} + + +//------------------------------------------------------------------------------------------------- +// Object representing a single reaction +//------------------------------------------------------------------------------------------------- + +class Reaction { + LinkedList reactants; + LinkedList inhibitors; + LinkedList products; + + public Reaction() { + reactants = new LinkedList(); + inhibitors = new LinkedList(); + products = new LinkedList(); + } + + public Reaction(Reaction rr) { + reactants = new LinkedList(rr.reactants); + inhibitors = new LinkedList(rr.inhibitors); + products = new LinkedList(rr.products); + } + + public Set getReactantsSet() { + Set rset = new HashSet(); + rset.addAll(reactants); + rset.addAll(inhibitors); + rset.addAll(products); + + return rset; + } + + public String toRSSLString() { + return " {" + "{" + reactants.toString().replace("[", "").replace("]", "") + "}, " + + "{" + inhibitors.toString().replace("[", "").replace("]", "") + "} -> " + + "{" + products.toString().replace("[", "").replace("]", "") + "}" + + "};\n"; + } + + public void exportToXML(PrintWriter output) { + output.println(" "); + + for (String str : reactants) + output.println(" " + str + ""); + + for (String str : inhibitors) + output.println(" " + str + ""); + + for (String str : products) + output.println(" " + str + ""); + + output.println(" "); + } +} diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java new file mode 100644 index 0000000..14a46e1 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactantSetPanel.java @@ -0,0 +1,49 @@ +package pl.umk.mat.martinp.reactics; + +import javax.swing.*; +import javax.swing.border.LineBorder; +import javax.swing.border.TitledBorder; +import java.awt.*; +import java.util.*; +import java.util.stream.Collectors; + + +public class ReactantSetPanel extends JPanel implements RSObserver { + private final int borderThickness = 2; + + JTextArea textArea = new JTextArea(); + + public ReactantSetPanel() { + textArea.setEditable(false); + textArea.setLineWrap(true); + textArea.setWrapStyleWord(false); + Font textFont = textArea.getFont(); + textArea.setFont(new Font(textFont.getFamily(), Font.BOLD, textFont.getSize()+2)); + + this.setPreferredSize(new Dimension(-1, 75)); + + this.setLayout(new BorderLayout()); + this.add(new JScrollPane(textArea), BorderLayout.CENTER); + + TitledBorder outBorder = BorderFactory.createTitledBorder("Reactants"); + Font borderFont = outBorder.getTitleFont(); + outBorder.setTitleFont(new Font (borderFont.getFamily(), Font.BOLD, borderFont.getSize()+2)); + outBorder.setBorder(new LineBorder(Color.black, borderThickness, true)); + setBorder(outBorder); + } + + public void updateReactants(Set reactantsSet) { + textArea.setText(""); +// textArea.setText(Arrays.toString(reactantsSet.toArray())); + textArea.setText(Arrays.stream(reactantsSet.toArray()).map(String::valueOf).collect(Collectors.joining(" "))); + } + + public void clear() { + textArea.setText(""); + } + + public void onRSUpdate() { + ReactionSystem rs = ReactionSystem.getInstance(); + updateReactants(rs.getReactants()); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java new file mode 100644 index 0000000..10d126e --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsGUI.java @@ -0,0 +1,791 @@ +/** Main application window */ + +package pl.umk.mat.martinp.reactics; + +import org.w3c.dom.Document; +import org.xml.sax.SAXException; +import javax.swing.*; +import javax.swing.filechooser.FileNameExtensionFilter; +import javax.xml.parsers.DocumentBuilder; +import javax.xml.parsers.DocumentBuilderFactory; +import javax.xml.parsers.ParserConfigurationException; +import java.awt.*; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.io.*; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.StandardOpenOption; +import java.util.Collection; +import java.util.TreeSet; + + +public class ReacticsGUI extends JFrame { + public final static String ApplicationName = "ReactICS GUI"; + public final static String ApplicationVersion = "0.1"; + public final static String ApplicationReleaseDate = "2025"; + + private static final String defaultConfigFileName = "reactics.conf"; + + private JFrame window; + private JTabbedPane modulePane; + private ReactantSetPanel reactantSetPanel; + private ReactionSystemEditor reactionSystemEditor; + private ContextAutomatonEditor contextAutomatonEditor; + private TransitionSystemViewer transitionSystemViewer; + private TransitionSystemViewer compressedTransitionSystemViewer; + private FormulaEditor formulaEditor; + + private FileSelector fileSelector; + + private ReactionSystem reactionSystem; + private ReacticsRuntime reactics; + + + public ReacticsGUI() { + super(ApplicationName); + + reactionSystem = ReactionSystem.getInstance(); + + try { + reactics = ReacticsRuntime.getInstance(); + } + catch (ReacticsRuntimeException rre) { + JOptionPane.showMessageDialog(this, + rre.getMessage(), + "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE); + } + + Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); + setSize(new Dimension(screenSize.width-200, screenSize.height-200)); + createMenuBar(); + createContentPane(); + + fileSelector = FileSelector.getInstance(); + + try { + reactics.loadConfig(defaultConfigFileName); + } + catch (ConfigReadingError cre) { + System.err.println("[ReactICS] Error reading configuration: " + cre.getMessage()); + JOptionPane.showMessageDialog(this, + "Could not read configuration\n" + cre.getMessage(), + "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE); + } + catch (InvalidRuntimeException ire) { + System.err.println("[ReactICS] ReactICS runtime cannot be executed" + ire.getMessage()); + JOptionPane.showMessageDialog(this, + "Invalid ReactICS runtime patn\n" + ire.getMessage() + + "\nYou may proceed with editing reaction system structure," + + "however not model checking will be possible.", + "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE); + } + + window = this; + } + + private void createMenuBar() { + JMenuBar menuBar = new JMenuBar(); + + JMenu fileMenu = new JMenu("File"); + menuBar.add(fileMenu); + + JMenuItem xmlLoadItem = new JMenuItem("Load from XML file"); + xmlLoadItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + loadFromXML(); + } + }); + fileMenu.add(xmlLoadItem); + + JMenuItem xmlsaveItem = new JMenuItem("Save to XML file"); + xmlsaveItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + saveAsXML(); + } + }); + fileMenu.add(xmlsaveItem); + + JMenuItem rsslImportItem = new JMenuItem("Import from RSSL file"); + rsslImportItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + importFromRSSL(); + } + }); + fileMenu.add(rsslImportItem); + + JMenuItem rsslExportItem = new JMenuItem("Save to RSSL file"); + rsslExportItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + exportToRSSLFile(); + } + }); + fileMenu.add(rsslExportItem); + + JMenuItem isplExportItem = new JMenuItem("Export to ISPL file"); + isplExportItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { exportToISPLFile(); } + }); + fileMenu.add(isplExportItem); + + JMenuItem exitItem = new JMenuItem("Exit"); + exitItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + System.exit(0); + } + }); + fileMenu.addSeparator(); + fileMenu.add(exitItem); + + JMenu helpMenu = new JMenu("Help"); + menuBar.add(helpMenu); + + JMenuItem helpItem = new JMenuItem("Help"); + helpItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { showHelpWindow(); } + }); + helpMenu.add(helpItem); + + JMenuItem aboutItem = new JMenuItem("About"); + aboutItem.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { showAboutWindow(); } + }); + helpMenu.add(aboutItem); + + setJMenuBar(menuBar); + } + + private void createContentPane() { + modulePane = new JTabbedPane(); + modulePane.setTabPlacement(JTabbedPane.NORTH); + + //----------------------------------------------------------------------------------------- + // Reaction System Editor + //----------------------------------------------------------------------------------------- + + reactionSystemEditor = new ReactionSystemEditor(); + modulePane.addTab("Reaction System", reactionSystemEditor); + reactionSystem.addObserver(reactionSystemEditor); + + + //----------------------------------------------------------------------------------------- + // Context Automaton Editor + //----------------------------------------------------------------------------------------- + + contextAutomatonEditor = new ContextAutomatonEditor(getSize()); + modulePane.addTab("Context Automaton", contextAutomatonEditor); + reactionSystem.addObserver(contextAutomatonEditor); + + + //----------------------------------------------------------------------------------------- + // Transition System Viewer + //----------------------------------------------------------------------------------------- + + JPanel transitionSystemPanel = new JPanel(new BorderLayout()); + transitionSystemViewer = new TransitionSystemViewer(getSize(), false); + transitionSystemPanel.add(transitionSystemViewer, BorderLayout.CENTER); + reactionSystem.addObserver(transitionSystemViewer); + + JPanel tsCtrlPanel = new JPanel(); + JButton tsUpdateBtn = new JButton("Update transition system"); + tsUpdateBtn.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { updateTransitionSystem(); } + }); + tsCtrlPanel.add(tsUpdateBtn); + + JCheckBox tsLockCBox = new JCheckBox("Lock relative nodes positions"); + tsLockCBox.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + transitionSystemViewer.lockNodesPositions(tsLockCBox.isSelected()); + } + }); + tsCtrlPanel.add(tsLockCBox); + + transitionSystemPanel.add(tsCtrlPanel, BorderLayout.NORTH); + modulePane.addTab("Transition System", transitionSystemPanel); + + //----------------------------------------------------------------------------------------- + // Compressed Transition System Viewer + //----------------------------------------------------------------------------------------- + + JPanel compressedTransitionSystemPanel = new JPanel(new BorderLayout()); + compressedTransitionSystemViewer = new TransitionSystemViewer(getSize(), true); + compressedTransitionSystemPanel.add(compressedTransitionSystemViewer, BorderLayout.CENTER); + reactionSystem.addObserver(compressedTransitionSystemViewer); + + JPanel ctsCtrlPanel = new JPanel(); + JButton ctsUpdateBtn = new JButton("Update transition system"); + ctsUpdateBtn.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { updateTransitionSystem(); } + }); + ctsCtrlPanel.add(ctsUpdateBtn); + + JCheckBox ctsLockCBox = new JCheckBox("Lock relative nodes positions"); + ctsLockCBox.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + compressedTransitionSystemViewer.lockNodesPositions(ctsLockCBox.isSelected()); + } + }); + ctsCtrlPanel.add(ctsLockCBox); + + compressedTransitionSystemPanel.add(ctsCtrlPanel, BorderLayout.NORTH); + modulePane.addTab("Compressed Transition System", compressedTransitionSystemPanel); + + //----------------------------------------------------------------------------------------- + // Formula Editor + //----------------------------------------------------------------------------------------- + + JPanel formulaEditorPanel = new JPanel(); + formulaEditorPanel.setLayout(new BorderLayout()); + formulaEditor = new FormulaEditor(reactionSystem); + reactionSystem.addObserver(formulaEditor); + formulaEditorPanel.add(formulaEditor, BorderLayout.CENTER); + + JPanel formulaCtrlPanel = new JPanel(); + JButton addButton = new JButton("Add formula"); + addButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { formulaEditor.addFormula(window); } + }); + formulaCtrlPanel.add(addButton); + + JButton edtButton = new JButton("Edit formula"); + edtButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + formulaEditor.editFormula(window); + } + }); + formulaCtrlPanel.add(edtButton); + + JButton rmButton = new JButton("Remove formulas"); + rmButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + formulaEditor.removeFormulas(); + } + }); + formulaCtrlPanel.add(rmButton); + + JButton evalButton = new JButton("Evaluate"); + evalButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + evaluateFormulas(); + } + }); + formulaCtrlPanel.add(evalButton); + + JButton resetButton = new JButton("Reset"); + resetButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + formulaEditor.resetFormulasStatus(); + } + }); + formulaCtrlPanel.add(resetButton); + + formulaEditorPanel.add(formulaCtrlPanel, BorderLayout.NORTH); + + //----------------------------------------------------------------------------------------- + // Split the main window into two parts. The upper one contains details of the reaction + // system. The bottom part contains the list of formulas for model checking. + //----------------------------------------------------------------------------------------- + + JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, modulePane, formulaEditorPanel); + splitPane.setResizeWeight(0.75); +// splitPane.setOneTouchExpandable(true); + splitPane.setDividerSize(8); + + getContentPane().setLayout(new BorderLayout()); + getContentPane().add(splitPane, BorderLayout.CENTER); + + //----------------------------------------------------------------------------------------- + // Update button + Reactant Set Viewer + //----------------------------------------------------------------------------------------- + + JPanel topPanel = new JPanel(); + topPanel.setLayout(new BorderLayout()); + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new BoxLayout(buttonPanel, BoxLayout.Y_AXIS)); + + JButton updateButton = new JButton("
Update
Reaction System
"); + updateButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + updateReactionSystem(); + } + }); + buttonPanel.add(updateButton); + topPanel.add(buttonPanel, BorderLayout.WEST); + reactantSetPanel = new ReactantSetPanel(); + reactionSystem.addObserver(reactantSetPanel); + topPanel.add(reactantSetPanel, BorderLayout.CENTER); + getContentPane().add(topPanel, BorderLayout.NORTH); + } + + private boolean isModified() { + return reactionSystemEditor.isModified() || contextAutomatonEditor.isModified(); + } + + private void clearModificationStatus() { + reactionSystemEditor.clearModificationStatus(); + contextAutomatonEditor.clearModificationStatus(); + transitionSystemViewer.clearModificationStatus(); + compressedTransitionSystemViewer.clearModificationStatus(); + } + + private void updateReactionSystem() { + System.out.println("[ReactICS] Update reaction system structure"); + + Path rsslFile = reactics.getRSSLFile(); + + try { + Files.writeString(rsslFile, ""); + + PrintWriter rsslStream = new PrintWriter(Files.newBufferedWriter(rsslFile)); + printRSStructure(rsslStream); + rsslStream.close(); + } + catch (IOException ie) { + System.err.println("[ReactICS] Could not read transition system structure: " + ie.getMessage()); + + JOptionPane.showMessageDialog(this, + "Could not read transition system structure\n" + ie.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + + reactionSystem.notifyObservers(); + updateReactantSet(); + clearModificationStatus(); + } + + private void updateReactantSet() { + TreeSet rset = new TreeSet(); + + rset.addAll(reactionSystemEditor.getReactantsSet()); + rset.addAll(contextAutomatonEditor.getReactantsSet()); + rset.remove(""); + reactantSetPanel.updateReactants(rset); + } + + private void updateTransitionSystem() { + if (isModified()) { + updateReactionSystem(); + } + else if (transitionSystemViewer.isComputed()) { + // Skip re-computing transition system structure + return; + } + + try { + String tsStructure = reactics.getTransitionSystemStructure(); + transitionSystemViewer.updateTransitionSystemStructure(tsStructure); + compressedTransitionSystemViewer.updateTransitionSystemStructure(tsStructure); + } + catch (IOException ioe) { + System.out.println("[ReactICS] I/O Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, + "Could not write reaction system structure to a temporary file\n" + ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + catch (ReacticsRuntimeException rre) { + System.out.println("[ReactICS] Runtime Error: " + rre.getMessage()); + JOptionPane.showMessageDialog(this, + rre.getMessage(), + "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE); + } + } + + private void evaluateFormulas() { + Collection formulas = formulaEditor.getSelectedFormulas(); + + if (isModified()) + updateReactionSystem(); + + Path rsslFile = reactics.getRSSLFile(); + long originalSize = -1; + + try { + originalSize = Files.size(rsslFile); + } + catch (IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + + for (Formula ff : formulas) { + try { + System.out.println("[ReactICS] Evaluate formula: " + ff.label); + + Files.writeString(rsslFile, ff.toRSSLString() + "\n", StandardCharsets.UTF_8, StandardOpenOption.APPEND); + + ReacticsRuntime.EvalResult result = reactics.evaluateFormula(ff.label); + ff.status = result.result(); + ff.mcTime = result.mcTime() + " s"; + ff.totalTime = result.totalTime() + " s"; + ff.memory = result.memory() + " MB"; + formulaEditor.refreshStatus(); + } + catch(IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + catch(ReacticsRuntimeException rre) { + System.err.println("[ReactICS] Runtime error: " + rre.getMessage()); + JOptionPane.showMessageDialog(this, + rre.getMessage(), + "Reactics Runtime Error", JOptionPane.ERROR_MESSAGE); + + ff.status = Formula.FormulaStatus.Invalid; + } + finally { + try { + RandomAccessFile raf = new RandomAccessFile(rsslFile.toFile(), "rw"); + raf.setLength(originalSize); + } + catch (IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + } + } + } + + private void saveAsXML() { + File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")), + new FileNameExtensionFilter("Reaction System (XML)", "xml")); + + if(outFile == null) + return; + + System.out.println("[ReactICS] Save to XML file: " + outFile.getName()); + + try { + PrintWriter xmlOut = new PrintWriter(new FileWriter(outFile)); + xmlOut.println(""); + reactionSystemEditor.exportToXML(xmlOut); + contextAutomatonEditor.exportToXML(xmlOut); + formulaEditor.exportToXML(xmlOut); + xmlOut.println(""); + xmlOut.flush(); + xmlOut.close(); + } + catch(IOException ioe) { + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + } + + private void loadFromXML() { + FileNameExtensionFilter fileTypeFilter = new FileNameExtensionFilter("Reaction System (XML)", "xml"); + JFileChooser fc = new JFileChooser(); + fc.addChoosableFileFilter(fileTypeFilter); + fc.setAcceptAllFileFilterUsed(true); + fc.setCurrentDirectory(new File(System.getProperty("user.dir"))); + + + if(fc.showOpenDialog(this) == JFileChooser.APPROVE_OPTION) { + File xmlFile = fc.getSelectedFile(); + loadFromXMLFile(xmlFile); + setTitle("ReactICS GUI : " + xmlFile.getName()); + } + + modulePane.setSelectedIndex(0); + clearModificationStatus(); + } + + + private void loadFromXMLFile(File xmlFile) { + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + transitionSystemViewer.clear(); + compressedTransitionSystemViewer.clear(); + + try { + DocumentBuilderFactory dbFactory = DocumentBuilderFactory.newInstance(); + DocumentBuilder dBuilder = dbFactory.newDocumentBuilder(); + Document doc = dBuilder.parse(xmlFile); + doc.getDocumentElement().normalize(); + reactionSystemEditor.loadFromXML(doc); + contextAutomatonEditor.loadFromXML(doc); + formulaEditor.loadFromXML(doc); + updateReactionSystem(); + } + catch(IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + + JOptionPane.showMessageDialog(this, "Error reading file: " + xmlFile.getName() + "\n" + ioe.getMessage(), + "Input error", JOptionPane.ERROR_MESSAGE); + + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + } + catch(ParserConfigurationException pce) { + System.err.println("[ReactICS] Parse Configuration Error: " + pce.getMessage()); + + JOptionPane.showMessageDialog(this, pce.getMessage(), + "Parse Configuration Error", JOptionPane.ERROR_MESSAGE); + + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + } + catch(SAXException se) { + System.err.println("[ReactICS] SAXException: " + se.getMessage()); + + JOptionPane.showMessageDialog(this, se.getMessage(), + "Parse error", JOptionPane.ERROR_MESSAGE); + + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + } + catch(FileStructureError err) { + System.err.println("[ReactICS]: File Structure Error: " + err.getMessage()); + + JOptionPane.showMessageDialog(this, err.getMessage(), + "XML file structure error", JOptionPane.ERROR_MESSAGE); + + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + } + catch(Exception e) { + System.out.println("[ReactICS] Error: " + e.getMessage()); + + JOptionPane.showMessageDialog(this, "Unexpected error reading file: " + xmlFile.getName() + + " " + e.getMessage(), + "Input error", JOptionPane.ERROR_MESSAGE); + + reactionSystemEditor.clear(); + contextAutomatonEditor.clear(); + reactantSetPanel.clear(); + } + } + + + private void importFromRSSL() { + FileNameExtensionFilter fileTypeFilter = new FileNameExtensionFilter("Reaction System Specification Language (rs)", "rs"); + JFileChooser fc = new JFileChooser(); + fc.addChoosableFileFilter(fileTypeFilter); + fc.setAcceptAllFileFilterUsed(true); + fc.setCurrentDirectory(new File(System.getProperty("user.dir"))); + + + if(fc.showOpenDialog(this) == JFileChooser.APPROVE_OPTION) { + File rsslFile = fc.getSelectedFile(); + + try { + File xmlFile = reactics.convertToXMLFile(rsslFile); + loadFromXMLFile(xmlFile); + } catch (IOException e) { + System.err.println("IOException: " + e.getMessage()); + e.printStackTrace(); + } catch (ReacticsRuntimeException e) { + System.err.println("ReacticsRuntimeException: " + e.getMessage()); + e.printStackTrace(); + } + + setTitle("ReactICS GUI : " + rsslFile.getName()); + contextAutomatonEditor.recalculateCoordinates(); + } + + modulePane.setSelectedIndex(0); + clearModificationStatus(); + } + + + private void exportToRSSLFile() { + File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")), + new FileNameExtensionFilter("Reaction System Specification Language (RSSL)", "rs")); + + if(outFile == null) + return; + + System.out.println("[ReactICS] Export to RSSL file: " + outFile.getName()); + + try { + PrintWriter rsslOut = new PrintWriter(new FileWriter(outFile)); + printRSStructure(rsslOut); + rsslOut.close(); + } + catch(IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + } + + + private void exportToISPLFile() { + updateReactionSystem(); + + if (!reactionSystem.isplTranslationAllowed()) { + JOptionPane.showMessageDialog(this, + "Context automaton contains guards for some transitions.\n" + + "Current version of ReactICS does not support translation to ISPL format in this case.\n", + "Translation is not possible", JOptionPane.INFORMATION_MESSAGE); + return; + } + + File outFile = fileSelector.selectOutputFile(this, new File(System.getProperty("user.dir")), + new FileNameExtensionFilter("Interpreted System Programming Language (ISPL)", "ispl")); + + if (outFile == null) + return; + + System.out.println("[ReactICS] Export to ISPL file: " + outFile.getAbsolutePath()); + + try { + if (!outFile.exists() && !outFile.createNewFile()) { + System.err.println("[ReactICS] Error: The file "+ outFile.getName() + " could not be created."); + JOptionPane.showMessageDialog(this, + "The file " + outFile.getName() + " could not be created.", + "Error", JOptionPane.ERROR_MESSAGE); + return; + } + + if (!outFile.canWrite()){ + System.err.println("[ReactICS] Error: Cannot write to the file " + outFile.getName()); + JOptionPane.showMessageDialog(this, + "Cannot write to the file " + outFile.getName(), + "Error", JOptionPane.ERROR_MESSAGE); + return; + } + + reactics.exportToISPLFile(outFile); + } + catch(IOException ioe) { + System.err.println("[ReactICS] Error: " + ioe.getMessage()); + JOptionPane.showMessageDialog(this, ioe.getMessage(), + "Error", JOptionPane.ERROR_MESSAGE); + } + catch(ReacticsRuntimeException rre) { + System.err.println("[ReactICS] Runtime error: " + rre.getMessage()); + JOptionPane.showMessageDialog(this, + rre.getMessage(), + "ReactICS Runtime Error", JOptionPane.ERROR_MESSAGE); + } + } + + private void printRSStructure(PrintWriter outStream) { + outStream.println("options { use-context-automaton; make-progressive; };\n"); + outStream.println(reactionSystemEditor.toRSSLString()); + outStream.println(contextAutomatonEditor.toRSSLString()); + } + + private void showAboutWindow() { + AboutWindow awin = AboutWindow.getInstance(); + awin.show(this); + } + + private void showHelpWindow() { + HelpWindow hwin = HelpWindow.getInstance(); + hwin.show(this); + } + + public static void main(String args[]) { + ReacticsGUI wnd = new ReacticsGUI(); + wnd.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + wnd.setLocationRelativeTo(null); + wnd.setVisible(true); + } + +} + + +//------------------------------------------------------------------------------------------------- +// Class responsible for selecting a file to load / save the reaction system structure +//------------------------------------------------------------------------------------------------- + +class FileSelector { + private enum Status {SELECT, APPROVE, CANCEL} + + private static FileSelector instance = null; + + public static synchronized FileSelector getInstance() { + if (instance == null) + instance = new FileSelector(); + + return instance; + } + + private FileSelector() { } + + public File selecInputFile(Component parent, File rootDir, FileNameExtensionFilter filter) { + Status opStatus = Status.SELECT; + JFileChooser fc = new JFileChooser(); + fc.addChoosableFileFilter(filter); + fc.setAcceptAllFileFilterUsed(true); + fc.setCurrentDirectory(rootDir); + File outFile = null; + + do { + if (fc.showOpenDialog(parent) != JFileChooser.APPROVE_OPTION) { + opStatus = Status.CANCEL; + break; + } + + outFile = fc.getSelectedFile(); + opStatus = Status.APPROVE; + + if(outFile.exists()) { + if (JOptionPane.showConfirmDialog(parent, + "The file " + outFile.getName() + " already exists.\n" + + "Do you wish to overwrite it?", "Warning", + JOptionPane.YES_NO_OPTION, JOptionPane.WARNING_MESSAGE) == JOptionPane.NO_OPTION) { + opStatus = Status.SELECT; + } + } + } while(opStatus == Status.SELECT); + + if(opStatus != Status.APPROVE) + outFile = null; + + return outFile; + } + + public File selectOutputFile(Component parent, File rootDir, FileNameExtensionFilter filter) { + Status opStatus = Status.SELECT; + JFileChooser fc = new JFileChooser(); + fc.addChoosableFileFilter(filter); + fc.setAcceptAllFileFilterUsed(true); + fc.setCurrentDirectory(rootDir); + File outFile = null; + + do { + if (fc.showSaveDialog(parent) != JFileChooser.APPROVE_OPTION) { + opStatus = Status.CANCEL; + break; + } + + outFile = fc.getSelectedFile(); + opStatus = Status.APPROVE; + + if(outFile.exists()) { + if (JOptionPane.showConfirmDialog(parent, + "The file " + outFile.getName() + " already exists.\n" + + "Do you wish to overwrite it?", "Warning", + JOptionPane.YES_NO_OPTION, JOptionPane.WARNING_MESSAGE) == JOptionPane.NO_OPTION) { + opStatus = Status.SELECT; + } + } + } while(opStatus == Status.SELECT); + + if(opStatus != Status.APPROVE) + outFile = null; + + return outFile; + } +} + + +/** + * General exception class for any error related to input XML file + */ +class FileStructureError extends Exception { + public FileStructureError(String message) { + super(message); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java new file mode 100644 index 0000000..d8c73ea --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReacticsRuntime.java @@ -0,0 +1,198 @@ +package pl.umk.mat.martinp.reactics; + +import java.io.*; +import java.nio.file.Files; +import java.nio.file.Path; + + +public class ReacticsRuntime { + private static ReacticsRuntime instance = null; + + private String rctPath = "./"; + private String rctRuntime = "reactics"; + private Path rsslFile; + + public static synchronized ReacticsRuntime getInstance() throws ReacticsRuntimeException { + if (instance == null) + instance = new ReacticsRuntime(); + + return instance; + } + + private ReacticsRuntime() throws ReacticsRuntimeException { + try { + rsslFile = Files.createTempFile("reaction_system_", ".rs"); + rsslFile.toFile().deleteOnExit(); + System.out.println("[ReactICS] Created temporary file: " + rsslFile.toAbsolutePath()); + } + catch (IOException e) { + System.err.println("[ReactICS] Problem creating temporary file: + e.getMessage()"); + throw new ReacticsRuntimeException("Problem creating temporary file:\n" + e.getMessage()); + } + } + + public Path getRSSLFile() { + return rsslFile; + } + + public void loadConfig(String configFileName) throws ConfigReadingError, InvalidRuntimeException { + System.out.println("[ReactICS] Loading configuration from: " + configFileName); + + try { + BufferedReader inputStream = new BufferedReader(new FileReader(configFileName)); + String line; + + while ((line = inputStream.readLine()) != null) { + if (line.startsWith("runtime")) { + line = line.replaceAll("\\s", ""); + rctRuntime = line.substring(line.indexOf(":") + 1); + } + else if (line.startsWith("path")) { + line = line.replaceAll("\\s", ""); + rctPath = line.substring(line.indexOf(":") + 1); + } + } + } + catch (IOException e) { + throw new ConfigReadingError(e.getMessage()); + } + + File rctRntFile = new File(rctPath + rctRuntime); + + if (! (rctRntFile.exists() && rctRntFile.canExecute()) ) { + throw new InvalidRuntimeException(rctPath + rctRuntime + " cannot be executed"); + } + + System.out.println("[ReactICS] Using runtime: " + rctPath + rctRuntime); + } + + public EvalResult evaluateFormula(String fLabel) throws IOException, ReacticsRuntimeException { + // Drop "-B" option if verification time should not be measured + Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -B -c " + fLabel + " " + rsslFile.toAbsolutePath(), + null, new File(rctPath)); + + BufferedReader formResultStream = new BufferedReader(new InputStreamReader(proc.getInputStream())); + String line; + Formula.FormulaStatus result = Formula.FormulaStatus.None; + String mcTime = ""; + String totalTime = ""; + String memory = ""; + + while ((line = formResultStream.readLine()) != null) { + if (line.contains("holds")) { + result = Formula.FormulaStatus.True; + } + else if (line.contains("not hold")) { + result = Formula.FormulaStatus.False; + } + else if (line.startsWith("STAT")) { + String[] tokens = line.split(";"); + mcTime = tokens[2]; + totalTime = tokens[5]; + memory = tokens[4]; + } + + //TODO: Handle incorrect formulas + } + + StringBuilder errMsg = new StringBuilder(); + BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream())); + while ((line = procErrStr.readLine()) != null) { + errMsg.append(line).append("\n"); + } + + if (!errMsg.isEmpty()) + throw new ReacticsRuntimeException(errMsg.toString()); + + return new EvalResult(result, mcTime, totalTime, memory); + } + + /** Complete Transition System. Context automaton state included. */ + public String getTransitionSystemStructure() throws IOException, ReacticsRuntimeException { + Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -t -X " + rsslFile.toAbsolutePath(), + null, new File(rctPath)); + + String line; + StringBuilder tsString = new StringBuilder(); + BufferedReader procOutStr = new BufferedReader(new InputStreamReader(proc.getInputStream())); + while ((line = procOutStr.readLine()) != null) { + tsString.append(line).append("\n"); + } + + StringBuilder errMsg = new StringBuilder(); + BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream())); + while ((line = procErrStr.readLine()) != null) { + errMsg.append(line).append("\n"); + } + + if (!errMsg.isEmpty()) + throw new ReacticsRuntimeException(errMsg.toString()); + + return tsString.toString(); + } + + public void exportToISPLFile(File outFile) throws IOException, ReacticsRuntimeException { + Process proc = Runtime.getRuntime().exec(rctPath + rctRuntime + " -e " + rsslFile.toAbsolutePath() + " > " + outFile.getAbsolutePath(), + null, new File(rctPath)); + + String line; + BufferedReader procOutStr = new BufferedReader(new InputStreamReader(proc.getInputStream())); + PrintWriter isplOutStr = new PrintWriter(new FileWriter(outFile)); + while ((line = procOutStr.readLine()) != null) { + isplOutStr.println(line); + } + isplOutStr.close(); + + StringBuilder errMsg = new StringBuilder(); + BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream())); + while ((line = procErrStr.readLine()) != null) { + errMsg.append(line).append("\n"); + } + + if (!errMsg.isEmpty()) + throw new ReacticsRuntimeException(errMsg.toString()); + } + + + public File convertToXMLFile(File rsslInputFile) throws IOException, ReacticsRuntimeException { + File xmlFile = Files.createTempFile("_" + rsslInputFile.getName(), ".xml").toFile(); + xmlFile.deleteOnExit(); + + ProcessBuilder procBuilder = new ProcessBuilder(rctPath + rctRuntime, "-y", rsslInputFile.getAbsolutePath()); + procBuilder.redirectOutput(new File(xmlFile.getAbsolutePath())); + Process proc = procBuilder.start(); + + String line; + StringBuilder errMsg = new StringBuilder(); + BufferedReader procErrStr = new BufferedReader(new InputStreamReader(proc.getErrorStream())); + while ((line = procErrStr.readLine()) != null) { + errMsg.append(line).append("\n"); + } + + if (!errMsg.isEmpty()) + throw new ReacticsRuntimeException(errMsg.toString()); + + return xmlFile; + } + + + record EvalResult(Formula.FormulaStatus result, String mcTime, String totalTime, String memory) {} +} + +class ConfigReadingError extends Exception { + public ConfigReadingError(String message) { + super(message); + } +} + +class InvalidRuntimeException extends Exception { + public InvalidRuntimeException(String description) { + super(description); + } +} + +class ReacticsRuntimeException extends Exception { + public ReacticsRuntimeException(String description) { + super(description); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java new file mode 100644 index 0000000..51a86c9 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/ReactionSystemEditor.java @@ -0,0 +1,409 @@ +/** A component for editing the reaction system details */ + +package pl.umk.mat.martinp.reactics; + +import org.w3c.dom.Document; +import org.w3c.dom.Node; +import org.w3c.dom.NodeList; + +import javax.swing.*; +import java.awt.*; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.io.PrintWriter; +import java.util.Collections; +import java.util.HashSet; +import java.util.Set; +import java.util.Vector; + + +//------------------------------------------------------------------------------------------------- +/** A graphical component allowing edition and display of a distributed reaction system. + * A distributed reaction system contains a number of processes. + * Each process contains a list of reactions. + */ +public class ReactionSystemEditor extends JPanel implements RSObserver { + ReactionSystem rs; + private Vector procEditors = new Vector(); + private JPanel processPanel = new JPanel(); + + + public ReactionSystemEditor() { + rs = ReactionSystem.getInstance(); + + processPanel.setLayout(new BoxLayout(processPanel, BoxLayout.Y_AXIS)); + + final Dimension buttonSize = new Dimension(150, 25); + + JButton addButton = new JButton("New process"); + addButton.setMaximumSize(buttonSize); + addButton.setPreferredSize(buttonSize); + addButton.setMaximumSize(buttonSize); + addButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + createProcess(); + } + }); + + JButton rmButton = new JButton("Remove"); + rmButton.setMaximumSize(buttonSize); + rmButton.setPreferredSize(buttonSize); + rmButton.setMaximumSize(buttonSize); + rmButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + removeProcesses(); + } + }); + + JButton copyButton = new JButton("Copy"); + copyButton.setMaximumSize(buttonSize); + copyButton.setPreferredSize(buttonSize); + copyButton.setMaximumSize(buttonSize); + copyButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + copyProcesses(); + } + }); + + JButton renameButton = new JButton("Rename"); + renameButton.setMaximumSize(buttonSize); + renameButton.setPreferredSize(buttonSize); + renameButton.setMaximumSize(buttonSize); + renameButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + renameProcess(); + } + }); + + JButton upButton = new JButton("Move up"); + upButton.setMaximumSize(buttonSize); + upButton.setPreferredSize(buttonSize); + upButton.setMaximumSize(buttonSize); + upButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + moveSelectedUp(); + } + }); + + JButton downButton = new JButton("Move down"); + downButton.setMaximumSize(buttonSize); + downButton.setPreferredSize(buttonSize); + downButton.setMaximumSize(buttonSize); + downButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + moveSelectedDown(); + } + }); + + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new BoxLayout(buttonPanel, BoxLayout.Y_AXIS)); + + buttonPanel.add(addButton); + buttonPanel.add(rmButton); + buttonPanel.add(copyButton); + buttonPanel.add(renameButton); + buttonPanel.add(upButton); + buttonPanel.add(downButton); + + this.setLayout(new BorderLayout()); + this.add(new JScrollPane(processPanel), BorderLayout.CENTER); + this.add(buttonPanel, BorderLayout.WEST); + + createProcess(); + } + + public boolean isModified() { + boolean procModified = false; + + for (ProcessEditor pe : procEditors) + procModified |= pe.isModified(); + + return rs.modified | procModified; + } + + public void clearModificationStatus() { + for (ProcessEditor pe : procEditors) + pe.clearModificationStatus(); + + rs.modified = false; + } + + public Set getReactantsSet() { + HashSet rset = new HashSet(); + + for (ProcessEditor pe : procEditors) + rset.addAll(pe.getReactantsSet()); + + return rset; + } + + public void exportToXML(PrintWriter output) { + output.println(" "); + + for (ProcessEditor process : procEditors) + process.exportToXML(output); + + output.println(" "); + } + + public void loadFromXML(Document input) throws ReactionSystemStructureError { + NodeList rsSections = input.getElementsByTagName("reaction-system"); + + if (rsSections.getLength() == 0 || rsSections.getLength() > 1) { + throw new ReactionSystemStructureError("An XML file should contain a single reaction system description."); + } + + NodeList processList = rsSections.item(0).getChildNodes(); + + for (int idx=0; idx toRemove = new Vector(); + for (ProcessEditor edt : procEditors) { + if (edt.isSelected()) { + toRemove.add(edt); + } + } + + if (toRemove.size() == procEditors.size()) { + JOptionPane.showMessageDialog(this, "There should be at least a single process in the system.", + "Warning", JOptionPane.WARNING_MESSAGE); + return; + } + + for (ProcessEditor edt : toRemove) { + if (rs.removeProcess(edt.getProcess())) { + processPanel.remove(edt); + procEditors.remove(edt); + } + else { + JOptionPane.showMessageDialog(this, "Process " + edt.getLabel() + + " appears in a formula or a context automaton guard.\n" + + "Update them before removing the process.", + "Warning", JOptionPane.WARNING_MESSAGE); + } + } + + rs.modified = true; + revalidate(); + } + + private void copyProcesses() { + Vector toBeCopied = new Vector(); + + for (ProcessEditor edt : procEditors) { + if (edt.isSelected()) { + toBeCopied.add(edt); + } + } + + for (ProcessEditor edt : toBeCopied) { + ProcessEditor newEdt = new ProcessEditor(rs.copyProcess(edt.getProcess())); + processPanel.add(newEdt); + procEditors.add(newEdt); + } + + rs.modified = true; + revalidate(); + } + + private void renameProcess() { + ProcessEditor toRename = null; + boolean fail = false; + + for (ProcessEditor edt : procEditors) { + if (edt.isSelected()) { + if (toRename == null) { + toRename = edt; + } + else { + fail = true; + break; + } + } + } + + if (fail || toRename == null) { + JOptionPane.showMessageDialog(this, "Select a single process to rename.", "Select process", JOptionPane.WARNING_MESSAGE); + return; + } + + String idRegex = "[a-zA-Z][a-zA-Z_0-9:-]*"; + boolean idOk = false; + + do { + String newLabel = JOptionPane.showInputDialog(this, "Process name", toRename.getProcess().label); + if (newLabel == null) + return; + + newLabel = newLabel.trim(); + + if (!newLabel.matches(idRegex)) { + JOptionPane.showMessageDialog(this, + "Process name should start with a letter and may contain only:
" + + "letters, numbers, colons (:), underscores (_) and hyphens (-)", + "Error", JOptionPane.ERROR_MESSAGE); + } + else { + idOk = true; + rs.renameProcess(toRename.getProcess(), newLabel); + toRename.rename(newLabel); + rs.notifyObservers(); + } + } + while (!idOk); + + } + + private void moveSelectedUp() { + Vector toBeMovedIds = new Vector(); + for (int i = 0; i< procEditors.size(); ++i) { + if (procEditors.elementAt(i).isSelected()) + toBeMovedIds.add(i); + } + + for (int pos : toBeMovedIds) { + if (pos == 0 || procEditors.elementAt(pos-1).isSelected()) + continue; + + Collections.swap(procEditors, pos, pos-1); + } + + processPanel.removeAll(); + + for (ProcessEditor edt : procEditors) { + processPanel.add(edt); + } + + rs.modified = true; + revalidate(); + } + + private void moveSelectedDown() { + Vector toBeMovedIds = new Vector(); + + for (int i = procEditors.size()-1; i>=0; --i) { + if (procEditors.elementAt(i).isSelected()) + toBeMovedIds.add(i); + } + + for (int pos : toBeMovedIds) { + if (pos == procEditors.size()-1 || procEditors.elementAt(pos+1).isSelected()) + continue; + + Collections.swap(procEditors, pos, pos+1); + } + + processPanel.removeAll(); + + for (ProcessEditor edt : procEditors) { + processPanel.add(edt); + } + + rs.modified = true; + revalidate(); + } + + public void onRSUpdate() { + repaint(); + } + +} + + +class ReactionSystemStructureError extends FileStructureError { + public ReactionSystemStructureError(String message) { + super(message); + } +} \ No newline at end of file diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java new file mode 100644 index 0000000..b7083af --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionEditor.java @@ -0,0 +1,208 @@ +package pl.umk.mat.martinp.reactics; + +import javax.swing.*; +import javax.swing.table.AbstractTableModel; +import java.awt.*; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.util.*; + + +class TransitionEditor extends JDialog { + private JTable transitionsList; + private TransitionTableModel transitionsModel; + private Vector transitions; + + public TransitionEditor() { + super(); + + // Create reactions list component + transitionsModel = new TransitionTableModel(); + transitionsList = new JTable(transitionsModel); + + Font cellFont = transitionsList.getFont(); + Font headerFont = transitionsList.getTableHeader().getFont(); + + transitionsList.setFont(new Font("Monospaced", 0, cellFont.getSize() + 2)); + transitionsList.getTableHeader().setFont(new Font(headerFont.getFamily(), Font.BOLD, headerFont.getSize() + 2)); + transitionsList.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION); + + getContentPane().setLayout(new BorderLayout()); + + JButton addButton = new JButton("Add transition"); + addButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { addTransition(); } + }); + + JButton edtButton = new JButton("Edit transition"); + edtButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { editTransition(); } + }); + + JButton rmButton = new JButton("Remove transition"); + rmButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { removeTransitions(); } + }); + + JButton closeButton = new JButton("Close"); + closeButton.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { setVisible(false); } + }); + + JPanel buttonPanel = new JPanel(); + buttonPanel.add(addButton); + buttonPanel.add(edtButton); + buttonPanel.add(rmButton); + buttonPanel.add(closeButton); + + getContentPane().add(buttonPanel, BorderLayout.NORTH); + getContentPane().add(new JScrollPane(transitionsList), BorderLayout.CENTER); + + setPreferredSize(new Dimension(-1, 200)); + setSize(new Dimension(600, 200)); + setTitle("Transitions"); + } + + public void showTransitionEditDialog(Component parent, Collection trans, String from, String to) { + setTitle("Transitions for (" + from + " -> " + to + ")"); + transitions = (Vector) trans; + transitionsModel.fireTableDataChanged(); + setLocationRelativeTo(parent); + setVisible(true); + } + + private void addTransition() { + Transition tr = new Transition("", ""); + + if (!showTransitionEditDialog(tr)) + return; + + transitions.add(tr); + transitionsModel.fireTableDataChanged(); + } + + private void editTransition() { + int[] selected = transitionsList.getSelectedRows(); + + if (selected.length != 1) { + JOptionPane.showMessageDialog(this, "Select a single transition to edit.", "Select transition", JOptionPane.WARNING_MESSAGE); + return; + } + + Transition tr = transitions.get(selected[0]); + transitionsList.clearSelection(); + if (!showTransitionEditDialog(tr)) { + return; + } + + transitions.setElementAt(tr, selected[0]); + transitionsModel.fireTableDataChanged(); + } + + private void removeTransitions() { + int[] selected = transitionsList.getSelectedRows(); + + for (int trIdx : selected) { + transitions.remove(trIdx); + transitionsList.clearSelection(); + } + + transitionsModel.fireTableDataChanged(); + } + + private boolean showTransitionEditDialog(Transition tr) { + final int Select = 0; + final int Approve = 1; + + JTextField contextInput = new JTextField(30); + JTextField guardInput = new JTextField(30); + + String contextStr = tr.context; + String guardStr = tr.guard; + + contextInput.setToolTipText("Additional entities for processes"); + guardInput.setToolTipText("Initial conditions for the transition in rsCTL format."); + + JPanel myPanel = new JPanel(new GridBagLayout()); + GridBagConstraints cs = new GridBagConstraints(); + + cs.insets = new Insets(5, 5, 5, 5); + cs.anchor = GridBagConstraints.WEST; + cs.gridx = 0; + cs.gridy = 0; + myPanel.add(new JLabel("Context"), cs); + + cs.gridx = 1; + cs.gridy = 0; + myPanel.add(contextInput, cs); + + cs.gridx = 0; + cs.gridy = 1; + myPanel.add(new JLabel("Guards"), cs); + + cs.gridx = 1; + cs.gridy = 1; + myPanel.add(guardInput, cs); + + int opStatus = Select; + + do { + contextInput.setText(contextStr); + guardInput.setText(guardStr); + + int result = JOptionPane.showConfirmDialog(null, myPanel, + "Reaction details", JOptionPane.OK_CANCEL_OPTION); + + if (result != JOptionPane.OK_OPTION) { + return false; + } + + contextStr = contextInput.getText(); + guardStr = guardInput.getText(); + + //TODO: Validate the data entered to the text fields + tr.context = contextStr; + tr.guard = guardStr; + + opStatus = Approve; + } + while(opStatus == Select); + + return true; + } + + + class TransitionTableModel extends AbstractTableModel { + + private final String[] columnNames = {"Context", "Guard"}; + + public String getColumnName(int colIdx) { + return columnNames[colIdx]; + } + + public int getRowCount() { + return transitions.size(); + } + + public int getColumnCount() { + return columnNames.length; + } + + + public Object getValueAt(int row, int column) { + Transition tr = transitions.get(row); + + return switch (column) { + case 0 -> tr.context; + case 1 -> tr.guard; + default -> ""; + }; + } + + public boolean isCellEditable(int rowIndex, int columnIndex) { + return false; + } + } + +} + diff --git a/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java new file mode 100644 index 0000000..82c8949 --- /dev/null +++ b/reactics-gui/src/pl/umk/mat/martinp/reactics/TransitionSystemViewer.java @@ -0,0 +1,367 @@ +package pl.umk.mat.martinp.reactics; + +import edu.uci.ics.jung.algorithms.layout.*; +import edu.uci.ics.jung.algorithms.layout.util.Relaxer; +import edu.uci.ics.jung.graph.DirectedSparseGraph; +import edu.uci.ics.jung.visualization.VisualizationViewer; +import edu.uci.ics.jung.visualization.control.DefaultModalGraphMouse; +import edu.uci.ics.jung.visualization.control.ModalGraphMouse; +import edu.uci.ics.jung.visualization.decorators.ToStringLabeller; +import edu.uci.ics.jung.visualization.renderers.Renderer; +import org.apache.commons.collections15.Transformer; + +import javax.swing.JPanel; +import javax.swing.JToolTip; +import javax.swing.Icon; +import javax.swing.border.EtchedBorder; +import java.awt.*; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + + +public class TransitionSystemViewer extends JPanel implements RSObserver { + + //--------------------------------------------------------------- + // Visual configuration settings + //--------------------------------------------------------------- + + private static final Color pickedNodeColor = Color.yellow; + private static final Color edgeColor = Color.black; + private static final Font nodeLabelFont = new Font("Helvetica", Font.BOLD, 20); + private static final Font toolTipFont = new Font("Helvetica", Font.PLAIN, 14); + private static final Stroke basicEdgeArrow = new BasicStroke(3.0f); + + private static Dimension initialEditorSize; + + private VisualizationViewer graphViewer; + private Layout graphLayout; + DefaultModalGraphMouse graphMouse; + + //--------------------------------------------------------------- + // Transition system graph + //--------------------------------------------------------------- + + private DirectedSparseGraph tsGraph; + private boolean isCompressed; + + // Is transition system already computed? + // Used to avoid unnecessary computation of the same graph. + private boolean computed = false; + + // compressed == true => context automaton state is not taken into account. + public TransitionSystemViewer(Dimension size, boolean compressed) { + this.setLayout(new BorderLayout()); + tsGraph = new DirectedSparseGraph(); + this.isCompressed = compressed; + initialEditorSize = size; + + createGraphViever(); + lockNodesPositions(false); + } + + // Is transition system graph already computed? + boolean isComputed() { return computed; } + + void clearModificationStatus() { computed = false; } + + private void createGraphViever() { + graphLayout = new FRLayout(tsGraph); + + graphViewer = new VisualizationViewer(graphLayout, initialEditorSize) { + public JToolTip createToolTip() { + JToolTip tooltip = super.createToolTip(); + tooltip.setFont(toolTipFont); + return tooltip; + } + }; + + // Nodes labels + graphViewer.getRenderContext().setVertexLabelTransformer( + new ToStringLabeller()); + graphViewer.getRenderer().getVertexLabelRenderer() + .setPosition(Renderer.VertexLabel.Position.CNTR); + graphViewer.getRenderContext().setVertexFontTransformer( + new Transformer() { + public Font transform(TSState st) { + return nodeLabelFont; + } + }); + + // Nodes colour, background, etc. + graphViewer.getRenderContext().setVertexIconTransformer(new Transformer() { + public Icon transform(final TSState v) { + Color nodeColor = null; + + if(graphViewer.getPickedVertexState().isPicked(v)) + nodeColor = pickedNodeColor; + else + nodeColor = v.getFillColor(); + + return (v.isInitial() ? new SquareIcon(nodeColor, v.getWidth()) : new CircleIcon(nodeColor, v.getWidth())); + + }}); + + graphViewer.getRenderContext().setEdgeShapeTransformer(new ConditionalEdgeShape<>(1.5f)); + + // Edges + graphViewer.getRenderContext().setEdgeArrowStrokeTransformer(new Transformer() { + public Stroke transform(TSTransition tr) { + return basicEdgeArrow; + } + }); + + // For interactive graph editing + graphMouse = new DefaultModalGraphMouse(); + graphViewer.setGraphMouse(graphMouse); + graphMouse.setMode(ModalGraphMouse.Mode.PICKING); + + graphViewer.setVertexToolTipTransformer(new Transformer() { + public String transform(TSState st) { + return st.getTooltipText(); + } + }); + + graphViewer.setBackground(Color.white); + graphViewer.setBorder(new EtchedBorder(EtchedBorder.LOWERED)); + + add(graphViewer, BorderLayout.CENTER); + } + + + public void updateTransitionSystemStructure(String tsString) { + // Clear graph + clear(); + + // Load graph structure + int nextId = 1; + + HashMap nodes = new HashMap<>(); + TSState src = null; + + for (String line : tsString.split("\\R")) { + char type = line.charAt(0); + line = line.substring(2).strip(); + int end = line.lastIndexOf('}'); + String automatonState = line.substring(end + 1, line.length() - 1).strip(); + String stateStr = line.substring(line.indexOf('{'), end + 1); + TSState state = nodes.get( isCompressed ? stateStr : line); + + if (state == null) { + state = new TSState(nextId++, stateStr, isCompressed ? null : automatonState); + nodes.put(isCompressed ? stateStr : line, state); + tsGraph.addVertex(state); + } + + if (type == 'G') { + src = state; + } + else if (type == 's') { + tsGraph.addEdge(new TSTransition(), src, state); + } + } + + // Find the initial state + for (TSState state : tsGraph.getVertices()) { + if (tsGraph.getInEdges(state).size() == 0) { + state.setAsInitial(); + break; + } + } + + relax(); + graphViewer.repaint(); + computed = true; + } + + + public void lockNodesPositions(boolean lock) { + if (lock) + graphMouse.setMode(ModalGraphMouse.Mode.TRANSFORMING); + else + graphMouse.setMode(ModalGraphMouse.Mode.PICKING); + } + + + public void clear() { + for (TSState st : new java.util.ArrayList(tsGraph.getVertices())) { + tsGraph.removeVertex(st); + } + + repaint(); + } + + + /** For better vertex placement */ + private void relax() { + graphLayout.initialize(); + graphLayout.setSize(graphViewer.getSize()); + Relaxer relaxer = graphViewer.getModel().getRelaxer(); + + if (relaxer != null) { + relaxer.stop(); + relaxer.prerelax(); + relaxer.relax(); + } + } + + + //--------------------------------------------------------------------------------------------- + // For drawing the initial state + //--------------------------------------------------------------------------------------------- + + static class SquareIcon implements Icon { + private final Color fillColor; + private final int width; + + public SquareIcon(Color fColor, int width) { + fillColor = fColor; + this.width = width; + } + + public void paintIcon(Component c, Graphics g, int x, int y) { + g.setColor(fillColor); + g.fillRect(x, y, width, width); + g.setColor(Color.black); + g.drawRect(x, y, width, width); + } + + public int getIconWidth() { + return width; + } + + public int getIconHeight() { + return width; + } + } + + + //--------------------------------------------------------------------------------------------- + // For drawing all non-initial states + //--------------------------------------------------------------------------------------------- + + static class CircleIcon implements Icon { + private final Color fillColor; + private final int radius; + + public CircleIcon(Color fColor, int radius) { + fillColor = fColor; + this.radius = radius; + } + + public void paintIcon(Component c, Graphics g, int x, int y) { + g.setColor(fillColor); + g.fillOval(x, y, radius, radius); + g.setColor(Color.black); + g.drawOval(x, y, radius, radius); + } + + public int getIconWidth() { + return radius; + } + + public int getIconHeight() { + return radius; + } + } + + public void onRSUpdate() { + clear(); + } + +} + + +//------------------------------------------------------------------------------------------------- +// Single node of the Transition system graph +//------------------------------------------------------------------------------------------------- + +class TSState { + + public final static Color fillColor = Color.lightGray; + public final static Color initialColor = new Color(102, 178, 255); + + private static final int nodeWidth = 30; + private static final int nodeHeight = 30; + + private final int id; + private final String rsDetails; + private final String toolTipText; + private final String aState; + private boolean initial = false; + + public TSState(int id, String stateStr) { + this.id = id; + this.rsDetails = formatRSDetails(stateStr.substring(1, stateStr.length() - 1).strip()); + this.aState = null; + this.toolTipText = formatToolTipText(); + } + + public TSState(int id, String stateStr, String aState) { + this.id = id; + this.rsDetails = formatRSDetails(stateStr.substring(1, stateStr.length() - 1).strip()); + this.aState = aState; + this.toolTipText = formatToolTipText(); + } + + public boolean isInitial() { + return initial; + } + + public void setAsInitial() { + initial = true; + } + + public String toString() { + return String.valueOf(id); + } + + public int getWidth() { + return nodeWidth; + } + + public int getHeight() { + return nodeHeight; + } + + Color getFillColor() { + return initial ? initialColor : fillColor; + } + + public String getTooltipText() { + return toolTipText; + } + + private String formatRSDetails(String rsDetails) { + return rsDetails.replaceAll("\\} (proc\\d+=\\{)", "}
$1"); + } + + private String formatToolTipText() { + Pattern pattern = Pattern.compile("\\w+=\\{[^}]*\\}"); + Matcher matcher = pattern.matcher(rsDetails); + + ArrayList blocks = new ArrayList(); + + while (matcher.find()) { + blocks.add(matcher.group()); + } + + if (aState != null) + return "" + + "CA " + aState+ "
" + + String.join("
", blocks) + + ""; + else + return "" + + String.join("
", blocks) + + ""; + } +} + + +//------------------------------------------------------------------------------------------------- +// Single edge of the Transition system graph +//------------------------------------------------------------------------------------------------- + +class TSTransition { }