From 02d08eba0ef762d3f958d193ed5ac9c965fe685b Mon Sep 17 00:00:00 2001 From: RipplB Date: Sat, 14 Dec 2024 18:21:35 +0100 Subject: [PATCH] Add documentation --- .../theta/analysis/algorithm/asg/README.md | 13 +++ .../analysis/algorithm/loopchecker/README.md | 88 ++++++++++++++++++ subprojects/common/ltl-cli/README.md | 4 + subprojects/common/ltl/doc/README.md | 76 +++++++++++++++ subprojects/common/ltl/doc/ltl2buchi.drawio | 70 ++++++++++++++ subprojects/common/ltl/doc/ltl2buchi.jpg | Bin 0 -> 28328 bytes .../ltl/doc/ltl_conversion_pipeline.drawio | 31 ++++++ .../ltl/doc/ltl_conversion_pipeline.jpg | Bin 0 -> 7550 bytes subprojects/xsts/xsts-cli/README.md | 87 +++++++++-------- 9 files changed, 330 insertions(+), 39 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md create mode 100644 subprojects/common/ltl-cli/README.md create mode 100644 subprojects/common/ltl/doc/README.md create mode 100644 subprojects/common/ltl/doc/ltl2buchi.drawio create mode 100644 subprojects/common/ltl/doc/ltl2buchi.jpg create mode 100644 subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio create mode 100644 subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md new file mode 100644 index 0000000000..91de66f36c --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md @@ -0,0 +1,13 @@ +## Overview + +This package contains two new data structures, a Proof and a Cex. + +### Abstract State Graph + +`ASG` is a more simple state space representation than `ARG`. It works and is implemented in a very similar way, +except it does allow circles to appear in the graph. + +### ASG trace + +`ASGTrace` represents a lasso like trace, i.e. it is made with two parts: a tail and a loop. The loop is required +to start and end in the last state of the tail. This node in the graph is called honda. \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md new file mode 100644 index 0000000000..bd08f4b484 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md @@ -0,0 +1,88 @@ +## Overview + +This package provides algorithms that allow to look for accepting lasso shaped traces in a state space. +A lasso is a special form of trace, consisting of two parts: a tail and a loop. Both are like classic traces, where the +tail has to start from an initial state, and the loop has to start and end in the last state of the tail. +Loopchecker has to be provided with a predicate that can mark either states or actions as accepting. The loop checking +algorithms look for lasso traces that have such acceptance in their loop. + +## Data structures + +The data structures in Theta had a limitation that made them not suitable for the initial implementation of loopchecker. +Both ARG and Trace do not allow circles to appear in the state space. For this reason, loopchecker uses the +`hu.bme.mit.theta.analysis.algorithm.asg` package. + +## Algorithms +For abstraction and trace concretization there are 2-2 algorithms, completely interchangeable. This is implemented +using the strategy design pattern. + +### Abstraction + +During abstraction, the `ASG` is built and explored until a valid `ASGTrace` is found. There are currently two algorithms +implemented, both based on a dept first search. + +#### Nested Depth-First Search + +NDFS contains of two Depth-First searches right after eachother to find a lasso trace. The goal of the first DFS +is to find any acceptance, and than the second should find the very same acceptance from there. + +![]() + + +#### Guided depth first search + +The basis of the +algorithm is Depth-First Search (DFS), where we do only one search with a modified +condition instead of two nested ones compared to NDFS. Let us call encountering an accepting state/transition an acceptance. In the DFS, while keeping an acceptance counter, +look for a node that is already on the stack and has a smaller value on the counter +than the top of the stack. + +![]() + + +### Concretization + +Concretizing a lasso trace requires an extra step after simple concretization. First the lasso is straightened to a classic +trace, and a classic concretization is used to determine if it's even feasible. However, after that, one needs to make +sure that the loop of the lasso is also a possible loop in the concrete state space. + +#### Milano + +This is a more direct approach. It checks whether the honda can be in the same +state before and after the loop. This is done by adding the cycle validity constraint to the +loop. An expression is added to the solver that requires all variables to have the same value in the first and +last state of the loop. + +![]() + +#### Bounded unrolling + +The idea of bounded unwinding comes from E. Clarke et al., who defined an algorithm +to detect and refine lasso-shaped traces in the abstract state-space. The idea was that +even though we do not know if an abstract loop directly corresponds to a concrete loop, +we can be sure that the abstract loop can be concretized at most m different ways, where +m is the size of the smallest abstract state in the loop (if we think about abstract states as +sets of concrete states). That is because, if the loop is run m times and is concretizable, +the state that had the smallest number of concrete states has to repeat itself at least once. +The only limitations of the original algorithm were that it was defined for deterministic +operations only. + +To slightly mitigate this limitation and be able to use the algorithm, we need to eliminate as many nondeterministic operations as possible. To achieve this, nondeterministic +operations have to be unfolded: they are replaced with all their possible deterministic +counterparts. For the nondet operations of `xsts`, this can be seen in the `XstsNormalizerPass` pass object. + +Another limitation of the original algorithm in our context is that Theta is working with +possibly infinite domains, for which m could also potentially evaluate to infinite. To have a +chance to avoid these infinite unwindings, it is worth noting that counting all the concrete +states allowed by the abstract states in the loop is an overapproximation of the number +of all possible different states the concrete loop can reach. If a variable is included in only +such assignments (or no assignments at all) where the expression contains only literals, +that variable has a fixed value throughout the loop. That means, for such variables, just +one unwinding is enough. + +To find all the variables that contribute towards the needed number of unwindings, `VarCollectorStatementVisitor` is used. +![]() + +Since infinite bounds can +still be encountered, there is a configurable maximum for the bound. If m would be greater +than that, the refiner falls back to the default concretizer algorithm, which is Milano in the current implementation. diff --git a/subprojects/common/ltl-cli/README.md b/subprojects/common/ltl-cli/README.md new file mode 100644 index 0000000000..f839575586 --- /dev/null +++ b/subprojects/common/ltl-cli/README.md @@ -0,0 +1,4 @@ +## Overview +This package contains classes and objects related to CLIs that allow LTL model checking. For now it only contains a helper class +that is an implementation of the Clikt's package OptionGroup. This option group allows the user to select from the available +loopchecker and loop refinement strategies. \ No newline at end of file diff --git a/subprojects/common/ltl/doc/README.md b/subprojects/common/ltl/doc/README.md new file mode 100644 index 0000000000..bf0078de64 --- /dev/null +++ b/subprojects/common/ltl/doc/README.md @@ -0,0 +1,76 @@ +## Overview +This project has two main purposes. The `hu.bme.mit.theta.common.cfa.buchi` package is used to convert properties specified +in the LTL language to Buchi automata as CFA. The `hu.bme.mit.theta.common.ltl` package contains a SafetyChecker that +is able to perform LTL based model checking on any formalism. + +## Converting LTL to Buchi automaton + +The main job is done by implementations of the `Ltl2BuchiTransformer` interface. This accepts an LTL formula and +produces a Buchi automaton in Theta representation. The current implementation `Ltl2BuchiThroughHoaf` does the following: + +1. Preprocess the input LTL expression by substituting complex expressions with atomic propositions +2. Call a `Ltl2Hoaf` converter that produces the Buchi automaton in the [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/) +3. Use the `BuchiBuilder` object to read the HOAF string and generate a CFA + +![](ltl_conversion_pipeline.jpg) + +### Preprocessing +Linear Temporal Logic works with atomic propositions, i.e. variables and expressions can only be of type boolean. +In align to this, most tools won't accept complex formulae, like `F(x == 9)`, i.e. _x is eventually going to become 9_. +To support such expressions, a preprocessing step is implemented. The entry point is in the `ToStringVisitor` class. +This class creates a new, now valid LTL expression with only atomic propositions, and provides a mapping from these +propositions to the original expressions. In our previoues example, the result could be `F p0`, and the mapping would contain +`p0 -> x == 9`. + +### The purpose of [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/) in the implementation +Since there were no tools or libraries that could have been linked due to licensing issues, it was required +to support calling external tools. HOAF is a standard that has many advantages for us: + +* It's widely accepted and adopted by most of the tools related to LTL manipulation +* It's a rather stable but still maintained standard +* There is a library which is now included with theta that provides interfaces to work with HOAF + +This allows the end-user to use any tool for the conversion they'd like. They only need to provided a command that runs on their system +and when the `ExternalLtl2Hoaf` runs it by appending the processed LTL formula after it, returns a Buchi automaton in the HOA format. + +The recommended tools are [Spot](https://spot.lre.epita.fr/) and [Owl](https://owl.model.in.tum.de/). + + +### Why CFA? + +Implementing Buchi automaton from scratch would have resulted in a lot of duplicate code with the already existing CFA class. +For this reason, CFA is now extended with optional accepting states or edges. Such CFA can perfectly model a Buchi automaton. + +Of course, it would be more desirable, to have a common automaton superclass for CFA and a new Buchi automaton, but this was +not in scope for the project that developed these packages. + +### Automated testing of LTL checking + +Running external tools during automated testing such as in the CI/CD processes is not that feasible in the case of Theta. +For various reasons, our tests run on many different platforms. Running the above recommended programs during these tests +would result in a maintenance nightmare: + +* The tools would need to be installed on all runner images +* Since most of them are only distributed for linux, calling them would require to be different on different operating systems + * For example, on windows you might use `WSL`, but the command `wsl` would of course fail on a linux system + +For this reason, testing is done with another implementation of `Ltl2Hoaf`. `Ltl2HoafFromDir` is a class that expects +a directory as a parameter. Than when called with an LTL formula, encodes the formula to URL and looks up the resulting +filename.hoa in the directory. + +### Architecture + +The above interfaces and objects form the following architecture: + +![](ltl2buchi.jpg) + +## LTL checking + +In the ltl package there is a single class the `LtlChecker`. This is a subclass of the safety checker, so it can fit +into most CLI algorithms easily. It uses the conversion mechanisms to create a Buchi automaton. Then uses the +`hu.bme.mit.theta.analysis.multi` package to create a product of this buchi automaton and the model that needs to +be checket. Finally it simply constructs a loopchecker abstractor and refiner, than builds +a `CegarChecker` with them. + +For the details of the model checking algorithms, look at the `hu.bme.mit.theta.analysis.algorithm.loopchecker` package +in the common analysis subproject. \ No newline at end of file diff --git a/subprojects/common/ltl/doc/ltl2buchi.drawio b/subprojects/common/ltl/doc/ltl2buchi.drawio new file mode 100644 index 0000000000..27f8690cb9 --- /dev/null +++ b/subprojects/common/ltl/doc/ltl2buchi.drawio @@ -0,0 +1,70 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/subprojects/common/ltl/doc/ltl2buchi.jpg b/subprojects/common/ltl/doc/ltl2buchi.jpg new file mode 100644 index 0000000000000000000000000000000000000000..f58d526a38b02cef913179d438ac459432d2f6c1 GIT binary patch literal 28328 zcmeFZ2UJtd)-W6_2nZ@&x`c!dN^b(vNodkbC_-of0tN&G1bn1-NJ4K4gkGeDDk{Az zp?9fDRgkXWkN3Xsy4?TX=l!1dUElw$^{w^qtemsY%s#Vc&+I+t%8L_9RsNpQ4LFA@_W%H->l1f9HN`t7re=4pefs+y zzw@l&9*=*Y{{+s;P%u%(m*c(fSbVp z0RF>2(*DsVkFDLU|5n_U^W!CZdjMd!005vc1puf&0sv&NzvZ1D{-kbq&a;@$>*aR- za{#yi>;QKF5P&NH4iG%YgaP*eLICk!(*PyFjGFAvwSC)^*bB=c)fq z`1KAzNkW9U%zT*$2)IN^beWRqS37|9x2~Pn>$fWY2VA>Ke1+sPDcPmp`O3Ed0Aiv` zm#&hKT)py}?!134UA}Ua_!=b@H3`ja_EB0oppcP?cQU=Cg068=?Xa+fbt0aW1EeUT zXY&VGG$G`?6q*ag{|A@fsg(a<`k$#&0P=Glmnbh&0^|V)`Ttp`|MnSd!5>h<*z@fd zfc;eJ+h*nve6|4kmUBFy`$^?VsWVsG&#=AE9R^oQs=QU=yfS%zrd#}ApOnezYSK;& z&?-MoFa%JQ_sr7CPCY5vMS5?B*=|R%Zb=&+i#Hvp7yzJ6Tu)365rm4K+W9ILOe4Qv z&6@G@)YnN`vAnSmc0N4{Wm~BBbiql|kK|tf0u{fTn)?ZV)!ftv5t+7HyAh>sknEkU zHO*UAIW|fg$w~)J=UnGO5ISDyttfM_NJ?e?JFXu>r91^A@^k7Q)eH(gx z4a&%E93_Z&Dej5OmqZLfshdw)7}1Av5Y-WlIPs$+e*yUg*lrK+_N@K|SgZm40=(=# z(Ed`nJ&d!$IKQ=3tlYE`NiUCv4Xw=@ip99}+0*hcdc(;KZkMUVkC5Q}*}uo|0*}me zg&6Xx;*{h5fT520znvUUX~8A5YBsn#catd%Z%TC+SbJR)Tm$XWOWjmfiq@={RrfMsmbtFPv)K#ww{58I@+~_XbYnY0>eS1zW>N-Ni$*wNS%m(q&PD?zI_o^*o zEuA@AkIoges${t>0Cnk6O?>EnO5e9jCvvbTm&op4?XqBj!-2HK|CKiDX%Kb0-+8mB_wiV8V*xIA5LzQix)bV31ShKr5pSd zkU|j@?>_~>XxCh+t71qM4Up`r5Drt<7Pe{|4qY5qWKg+OfU$&V{&1N9U(|iG#g@vX zP2^x@K^lg#h!+Ezc{CfHMEFXIPs)7UA2lSRpd#B^cS*(kCt%ETq zD@@!&Z$5%Onc^mTgF*6(u1FmtWQoK0TUMLdNDRpupGUM)hQDOD5Oct113|uQ^w%UD zzR>W?^I>X6d#H60#0QFmC}or{m&DnY4Bh#lzgN^Jq9eTi zBJ@-vZzNVT|7A-Nw_e>REAX4{H$ccXdPeknp1lM{u{+s9cSTcubx!fU~Y_!mQIf|T&%+)t#<^3T+UQ2EW#_Dd5Rgk?<)EN zU#i6GYB@q7E6wIY4}(xpL7L>eOK%Yb4K-d={V}Y8f9)YyJ(C4Hu4|%=%?+*vnw`{m z(ftDO;O_Leesk{|5;5w9WK}p2zH5CEp!(cp=)5=F5`cQ{7lekgQ z*2Y#zFIeQBj{7#py_xD+?_Ta=u}kAu+IP&cdn;`gH3%P2@1Z{PE1FzkdCtb5Cq2p# zMT0y>&FC4(_KUMc7GS#cGrKL5+@M&C)z?1@;zr;VCd;n9p;}cq0sC1$)sUBSI#i^* zKnP=fbcDI&h@-e=n!w{y8QuU_T$hF+*PwSu5O4ls;M=pgH9;Hl(@R#ll_x(!mDq+{ z@=HVs=CLXvrk(G0NK;PHFwZvB!>djPkt8KB)Oafv)s^0VDt}@a(A+;f4UN)#NX;xhK;kNo| z&6>CIRhtk__HO;kUw{d_7Yhn%O0nWE#F(DRzw`Uf!npfFxqkTmQ2GsRtkSztGIx+X z?HW?R{!JwkfipfuqL z?%KGL`5_*M+j@gcI3ytk578U0z3vned0SSN|3^CfaBrfo!7yZ*m-mSI{wh#2k)iIu z>c$sq^-rqvU26<6LxZsm8%cu;4st>L64iu}t7e{cgG(7Y*sR>qm@M6b4D>HRyj$w- zDXY;B?jTQRoOYO8HK%Zt1k-L?{fU*Tgnd3sHF7-7Tzr=M=Z*Us)~zcz)m*{Lz{z&T z=7~VaDdpgHNuf}4qdrE!mjK*vgnUcW--%HH@@B@jGASn=(KtursCytNMp8~yQD#`K zy@y)Vq9}UHG3k`Jc*;T8VEQW~{UyzwidQuZHL7k@cH*iSp!RZElC82sN7#^?uwLcS zn72Vs)MfErchcfG_H75f8hd>txNQ3FA!dxqi9;CT;>Tk#9m2{5Wx0{AlCWH6uOnd^ zWh{fT2A}x!<2<*DAm;VWo$9NVjWo)eHlDY6gamXIud_Z_&Jfh|S@WR+Uw`FBz6*_gj!2{UP$x=;-pG9QGF= z$k*_@VAs2#ix(m1FSpH0YdS{~I4j}JXC(J8;D!&blw73!KYwGG@yWx$A}{|T5&4SY zOw})IaTAj!!?j++HL2e}+)HBiS=CGAS+Y1{ac|S%?_O!T$gb3v->(m0{F(Rb9PPvZOW0AKMS6`IpJ)gk zL=J*ukg=%rzA#~q9-jz)DXeKx9Sp^ZFr&eMslxlCqoYHf|F3P}qDC7kmzc_@G*a(e zayTmcMpg&_EKW@s4UK6uHe|GO-!e5%6}B>E$D1i?LCvuK?aIpb_8@w*NhY2Sj+rG< zdRC5JddU@K2>n;s9F`+g18Xk4ym*%a=_9BR9-sD)YbcpyORSka(FEq+s zSl*O@g0oIVbTEsogb&qGNvUV8DNgnbqbAJ}yljWo8VLW0P}Dd#GbG;c6$w<4-MN(U zyK~fpW`g{UlCb!;zE=kO(vxAr4eP`4nh@BmOT--9W!n*ICO&3sTTAJ3Uz`Q#X+?{H zM7}Te;K+o;>1)?>OVVzkD=d>RV&eUUk)COzU=lGDM52DA;sg|<7AVU-{5^=O*5sI1 zl-7hNbWo!cBGtYCogdz-KQ8xX{dwOqcA9PilF3q&)*;%R32{8(UKAqAlZu}x65$Xo z=QPX63K%0%tP{;Q7R5B;r^63PIlbdIv~vw`A(p8P+lFu4FuT>vWtgx0;D}Uw9@ zS|^Kz16C$_LaWbZQ8_X1dZn_MN1--io)&>@x1WQD;k?Je>l&Wm|vX&Q* z_)MsVIOT7$SdT*efK^^k;P3!Nn||15Adqp2lstS-K%* z3>%|JvZzX`6>z6*+HPLV6l>W?FHPDg)*DM^fnpIT+n2M&WqfXYKns0s8yC|498Cm2 zf70}T04T4FS8$2r9GG7nE8ZedO*=wwy#V2O1j57LC@af9xJ;-!89hbpxP^TS)U9M) zSHrpOmz)eQ&folWmTPl)R{gJycmIa!;^e1`!~CviV{BFB08=}6xzScM=Vw9xwjEYP zt%e;hl+l$O4RbLz=$;o?T&rgCh{@&$6dFF9C%>~<2fte?e@k4nwf zx}53xzvR_QkvEK+EGoJ7MJg{!$S>-Xh)gs^HHVgYr#gw*B9&eT>bt8jyX0_!?ofEw6`V`I8UrtlL#F8e8|VfFjEs+=6f_l+ocA|5-aDu?ef z$(u1FZ4qWVTO1thv6aL9m*zqP_>e*H?+7GK;$T^VNn3&)4+xt#i-3socc;5Vg~!<_ z1}qYdHFL>~`760skO^q_?1W8M_T*^3##{>dkwwBqGpR8Xnq9GqbK|)#p3v$zgNL4i zmJwn~hOQb!y<64S?VUgdx(zPHBu~D!D)&G^4J#(QwByqno%w|Kt+Hr)9DfYY#E+Z$ zFBU|}>TyI$r(J9zu zj>xLekTTdARDr`79;NmjqB(Hi_558+u4mcIE`QRWqkhn|pnh~zW_MI}>IY-WE?f!>72{bE zU8LY#D1wTZCau~#ynWiO-XY}Um@-o8TDEM`q0A8B&g8^Hnb7gBFW7DkpCz^#G!qp8 zqxX5fQJbYyT8~$Abr(w;9ORVsh|V@h&@sdIxe^o^6BtJ8Sa_H5s`elFKd!NzsaXns z>J!S&%ixqjyKvL{B{EBImS9eK)M-b=LW9#P`s@ArHHqE20 z7*dwD`?{Rj%yC_)eJRRXrV?v&O&(RdH6|yZD8nxRY0}E;cE~U@Z!g6uc%NCLQ4_6W zo~eakD0*nH_HCyy6-8{BhSt#Kb6=W0f28<@nHF(3;vwNnqBENmo6h<)BQtI+uOr}U z6i#_Qi}qx*!BbOqTB$rpYAr@{|E;Ju*V&31wu?p(qjWDd2S=R~VAiJKO@ux#AHLiZ zzqku~G#wj49e7}7fMXnSXh?&Q>e#1FGMfq;>v92ka<>BYv^N>pJDQZG2UPte z3jX=yysgeVm6eu9K43gw5m$73wdBsEyYjURdzn&cT>_T-;PFTqT4lhFcR_~~RKggN zPh%DoJ+tK6YL=Df&#%MVZk3z(XFB~RPXt? zi%V8b`kW$R2Rs{BS!#OH7Nz{HJ0}o$be_0DjO%GW(alRA~QWa z5K4NV)IoOIzS6R_u_Pizr2TjTa z4eu3RXDZ?C9lclourd8vc(0vuz83yqLE#kyl1ET!wN-_=NZr)aSI5T$0&}SGk0;&l zBT8aJ{sJVLk)5xD{nMo7 zUmq4%F20i$M;KKF3O(Ukyz*fO_K8-PfYf|FGLh`hce@QmZbNuARoJ4J=#bF;2d9t^ zJ$(7~3_am6x8X#)c7AroGJdF5ifcPbCnzhoJ9Y&fR0Rizk@kK?_ ztBsHVYyofY`u3Y}tgVqjoUQ|zus4>3@Fqx`n5GIP10#`lG9Q+^t0j1v9n z5b+tsrRdAyQTj^RhjLNddJjz){wf|uk*pr!wDJn}wYAvDsrjxN`#9pO+Hs5E0;)I>Bp}8=vj{$d({@n z9tF{I4xq@a><{nf8!{*FORI!6)if8J_;aB9MqMPy7+@o5Pi?tVj&ivO~s*4xrqs;_xPM6$Oi(E2RPz>%E00HI~Rum{Xa3$jea%P-cqUHD>KEKsnmN zH>z+Z|C|#UEJ3Za%AczZxekPSJ@Gx>)3sH#*9gr;EsNGL>Mh1NiE&4Hh_SBvrQE3f z><<P`P=L#Ot%FZE}I@CmH+-mr0F>&pp+=Wdut*!@u+K6D+Eu7C`8e`3FCw~n*077t;w z(^iALNvqPi=OKq6jqzsDQV%M8V_RRKsGR|K?H~`&@gt1K%>NJm6&@26qKwH+vtE%h z+vD%1P^$jK6FE$w1`=&9JAzhJkH+6&fi#TEx(88ZYg^lz3iKbF#d$|I1nQDSloZ`s zP%#KiS9EZ9hU^DUs!mek2}in}&s6HyZsa=4;T$GBZ|GzcCrQ7qxNE9b=$dcl0;;pk zCskvwLJzTbqRrc1FC;KzUy8TAJ8ou`p9<#x=?olhwkPBe9I#x*1BJ0a5qfnTpBo7u z5wP?GHpcML2KuKx?>kVDJ*B2bOP(ljM{rsvn++4Pend2DEjAGpPB>R~^z|W*yAR1< z?v{JU?0@##pAli5fv2(2F7-ya@EUxUx|lPZ48vs-cFZ}Vt@0?R?C zir!}>Z9)GBv%*;Xd1}fUHb)x_iwe`(3)q~5Ybv<8%#p-sGeR8KHUd)rLIgMwgP0#v ztha}7=tYM|HTQQJ+8fxK1u=ferxRk;oc1-{>TP`_oI4kAmps!|iAVbUlpjv= zr!N_!ywtD4E=Y8PFy*qGXy!#af7ga^hL@jyaXEXn9C?1+6M2>qs%f*p zS2*Rs)97$gV+2zAz{4;=f5noS1y{2%Ibe9Kllb&;@$>%=vQ%x)Up^DWkt$^l*ze>m zg!_Kb&!3>{RaJZplr!c&BuZtdstsqL8C5xLviH;C=l@1G;`aW?TDf`_zw%XgnNFrmk&WaxwALBJg?x#vcDj7*?s{Yars~9J+GwU3I{Rc z6*5rDF)^A8+`!(F~ z!^Ox^HHn8I=$n6NfDgZI`tFgZ=h5=rLp5&Q8a8pXxqC%YYn>nat;;q(PJvZ@{tsrY zf~NXmr?;-4a^?=_m0QlS2?p<$K(MEHi1Diz8Px;~0(+AF{td$hX z?<+T^m=|**^WPX(6~IULjRq&MBzoeWsF96?iCLcb2I5I7FAXO}S#=KS^R=kI1f<(7 zOFn0IIAfEf^h_VK8C>DrjOlB4k{_bl^KD@M_)LA*VyVVp{`hBPrgz_l!CwJLmj9}7 zH@wwKm2~g9_#T8w7UmRH7;Y9#?E4#5UT-gCE4c{!DIr%h5CIT2Q`on(=I&>wHy4+hL#SuZs4UOdLrtlE*6J^)Zkjw#DgSsGKIhk0|cURa*8tP%gcsA0d&mb~66OZ9Gfj9dl}Ndh1xQtg0x&0Vp-e?f-lvk(3X z%fHbO|26G%$%X#^CiK7Cgd(jvN60^0xtsImn(j6WC$qKfY^cI@6$(7Ed0nPM=TM`A zLEymmm!v>w1jHqGqW_S{nTYp>M^mAQ?f%wH1ayBL3sITzix6>#qVxn{J&;KR-Zk0G?LWV6Mgig!xnQ`8--l~Wv zNrrWvdl2hRY88YKFZ9*8nh&4G$5dfq4`h9K_aXiNV&wSWIb1wBO6)U7 zpZl6FTwOKz8@Z!&1F9sERyUJS>Q0O4^8|xCs%Cm9xMILxl)cP3XLLwQN2-$&IYRCW z$hO;N9syK^OS4UE^p^$~cDC$4b|ZN4%^qyZQTVjUXQRapUF;d2pa{+&WNMUNT<~I6 zyK|cbZ25p;H724O8}4;G(to#*kmgsf_K3JB z+-z;`(SFPvnDt8Xx+~{{Wbi$T0>;;FAw}T!8n9{^8k^SVt_zCt01}PO6o`IciqK6e z5bxg3Tbtp>ABR_nSg=UUYOCpnHZ%);4BnxRquWd;U6{3uI8jON61!$~yP_MlVcI}0 zGwG_^SsuuvD!K8kKnv~YBcN6ozu>7{g+X2AI&E99`cbl>gc${zoyEXDn*7Qq)Mu=AGb7R8NQHv?Mu%)kyE0;DXU)R*RgoCwtjd!tLBS_aiikBE zI_BGB;sQ?JJ;)r@a?dOZZU;6Giy~9Y4`BxHRmN`wd?V)Xb2D_ z?sp$5q}1UqYl(@UX-j9FQ>E&6prtzKj41x0oK1Fw?bB*pLT5m`(MdDq;i_mb)x2y( ze`k*7$1UEbs8Xr&yT)vwtPKNQL2J0i>qc}PNe`u&WN8CWt1#q*ltUo=aGS;}Lt}t_ znJR)0!X4o#S^~dY69?xw3xz#TTLZ6Fz%;9!rSr`kCoM4#_ zv)sp05V2N8I^%-xOSMB=cTl$$#EVFySlpOwt2q|LsKn>t)BXoSMLu1G>~C(+7Q2a~ zTmKZ4_dg6&a52fxtxXuW!@CW?VQ4m5^@o1!Dc47n3G3M}J`6^=mJ6;DpmJML9zwaF zPT9-%r6WNz)LP~Ny=_c?_%nh_KRd&q%iW%d;_GuU{YqN9TIM67)us%O#mkrO^a{&c5n?XpW$1@sjDU(3Vp`$u z@5KdESWWJ4_c^$b|KfpBT4t9qvsqsf2B~9Byq49R@u-ov9K^zxx zJAv8_4W36vQ(AA6>hZZ~MBwY~?@-Ep)&x;v>=xID=`yhFue@3xp+~34@ z={CgO_mO;>p{?d4M#~OO#wHTIqCQ<0EozY5rb;DfW|u9;CI5af)l;2t9QUChOX5b6kEWv9_4=U%NA|*@F{n$sQ+ngsJW)RZUCjwze%?tYRnGG8F{tfSO zGW?Um1zZVxs6Gp_FE%8&BIjf1h71b1CuY;P`!hlW1Vt$Gmx_8K6>7e+8EXW;K&qC7 zM|WC^SFPpsMi>tXhi3ml7GK3R?<&&^GES|}a&3<}1PiY**_zur3X3K@A8)=8OY=|N z;NrQYQM|i)&!>(sj9{OrL?cJE+<~@`g=IDK8e!DO6Lek$x`4D*VJ8j38b4NfhB=Zw zRcTB^tXA-G%&NP-ap~sX{h9WCpmACR+jDOT*UJG@*Gn3w&&%5C7iLB675ro(RHS;z zUAc&hs1)<8H+q8&^3Wd)uvxoJFB9H*S^oGI*igq8bk_3bY#=U9jc{4Limn`FywY61 zhoZOURPLs-e!VHmO(+t|@UH>FuH>cplrn|S+bquXJ?=cdV2>A7yw&cM7v*?+6GqPX zVtaeeVvq64m>K-gQzLdS6B`D)voRarXFs>DI1mKwuZLJxYc&v8D{8gl_=E+|LqnAV zUArpXegVE+ss69Rj}U2USrbm$G#Ti*P+74cy0N`#Yt@XR=sM2EPEC5Px{+Zhs#cH} zo5)kcMi%uXVOzVgA_g<-c1;%3hy)wPGSt@2N@~VQ5Qln)RTOyMM|; z%9u8mY_d9Oea=-h@fYCA)jMb{?;^W~1j;{}_19?O1s#R%oEDC-Ak+QO>!Fo0wQVqh*>T$v45AoBSuczROr6P-?=XC0&{pr)ixl6$;g`3;y~C0N=g@H%N+L8|7go|Pu`f$s$lTX2dQU#&vUVgt^QlDHPL849$a#%jI3^|jrXC~(F&`Yg|)*2BqxF2l+?2u>Jj(H z4YcMF-Lu+k(#^6cf4uO#u&9fv*i+dN|GRB90lgUJ$S$FD6Ut9Q4?`aBFiKJ#t1pRc zi@A%7`HmjM%?PM8Bx`uO9we;3o+~obYri%GSe~RTapj(&!p5`=ua;EZ+(+v{j@J66C)kek?&>S`LwCUulox)ZvcEV~pW%YE^0J z(P50TNFAnFk&h9IUW=Z|?e(lg3NUvWORt4*wtSD_DpoHKVh{V^Wp4a43Bf+`D$#MHfIW(%zl#c7+s=Vdp!`yJn{ zxIRBd9qaVmI2LiWI$t}kt-Bj|veoj_;+^~YYE?4ZdM&&YGFCD`X z0SoN19qv4)n@)WhXTw%BRjF$Q(egb2r%R45j)j`Q=`;3HRuhru8?&(D&arA69FNg3 z@8`4coU{CmjyG1h5~}2ydOq)eVAt4nyLppt);oFhsAZ5nK0_@i88ZKu)}F4=xy5x6~0IsY&yeEDhIqXsjmj#Wy(cG1m8jCyl0r>%YF74S?@Ep?b(X&zxeqH)bJ=VyRgx z@p(i3dL5rW&Mwj37IWz}PncG(f95A8KrnjXMbvKYh}NgU#$cTiDwP!}oXwuRAMLG7Emvv|AR(pU47*dq6cZ zROUpGj`)Y+`|1YkL0+tGZWwhvqeTd6rCNw0FY5U(zzj$H+_FO@m0?w4r5k4J-#g%l zIx7gwNnqmWQ7P%yv%__%?n4mILHY>V3KcoESB-BZ^a2t%hB)M{P`?2DqJiv*B6qO; zjWx$G*`i*U2+G!uikBVdXxaS>(Cu$JNF^{lmpKBtgr zn&A|n7P0I#w)ThIlkj-^N~uY6b%W3e6jBlkfgUy7pe!QOLGeY`@|?2N22?QC=5>_r zkh*)2+qdRyD^F5!09(vc-ErT6_)zB0wOvA;^+rf;G`7N%^$X3Pai=OV>z`vS%1VYG z{VZW@IQA4b6dvgHv&Ya(Xs}r4V3!Tv!EAL2HDy%Tg|wI)xcid8z!q_DV&sUfh;-`B z_m)O==d(q1-N}5&J-ceZ)P$BS*>3zK4CU=sdBNfHPg*sKI*Ty#3zscOO0m!Q^mJuV zdMdT0y0E~WxhUMid1wYCJB2y|?zc7u>_q_Y5`PL<i_j5Cn6D+`sR<`84s*#3(-BfA%MK^Utv=p1%M& zNjUg;3M+(;!rox&lie{cw?KrZCOo8S8)CbDYid3=xN!$;3$-RLcvz)J7hJ{*(F;hf z%x!Bv(js;(WN|3o4-^rIY>WB@aLqyW>RkH;kh8kEPt^2$)P7w+lPMCa=2(@?`W8_K zZyb~no7kjk>A4Hebrp`<(kNC)o{<+4W394#v%+VxYLr~a;Q4vhn>A^~=Stj3r;irK z-5_vZ1FD-s@tQbd?~VRyTo$Cw1E;!?sZ(@ZCR*^d?X5_0y6xfJ&83BDRDWvGy@lx^ z{SwN)S&Q%d_op|9+w$hze9k>Ir2PPLv_5+!oiV*kIcP z=}=DhI9HN#ww#mk4F#^Fa70>Wsj=o4SKahQ$yGxYXDU(r0`FilcGKG|x*$?<>Pd8i zWgHO?L|819%k>-G11edik^XA(-r?oQh~%A#*3Yv(bR5KW_8Lx_26qTZ(WTiQPd{9Z zfGX@8zV>n69;t=!>T!vhT$I*Scg2=Pmd=A$sSZe%&>Wt;M%8-5I1S`BSA3RcO2WW( zFs{wz=xJN^Bd$`X?}U5Hc3TMTmy8){4||IYNnHav=h-BuU=foQC)@UF9Ww~_1WX|s zKCNq*tL;HQI}o&eu>-cO_Q>qHZSZ48p`P|2RakY8V$>Glc!->l66{rEn2w)JZ}_=Rabs z7IIc3t3~VIgjON8vmK`37+z?yTw~>l>M(!!8y=AyS(%;+4jb873EewU0knCYuVOa5 zj7xk&aw)fW9KS03k{MP67a=uI)f=pidn%i>#;F_`6 zl1^fw1^df)+L4IzTwXb{^|T=dGn`yq^<_6qIw_;f?$H~#tM&DAwQR*386rcXddwInBT|Ln|Ar9`ZBw@D&x6xI`W^~g;-C4%^55URI6 zHtGHmxtqPPpS8h3_l@YEreSfO9RCz4PPCo(pK}BN!1HWgOK3oOO(*R*ppP$N`Bc8W zK~Awx03q3sBz2QsqEOu-vySNTcgcEh;~O*3`PY|p6clFjhCGASp+L?Z8#c#!hD=1mDMAoiGt%n-=MH(!nMqeui z?ZSMADeEijR*%UWonYu3(diqmJ9%kl^&=2)0;7SFUh`OtL3_2ugV1d@9dFpBudMl9 zaLz3kNmm^WN4+fJQ2QxTZB*e=rZ7+#NK|ux7_M;KH(u>DTx6dt(0-FUYL(7l93JEQ zHLvYxuuOjqd1`c%Q48Ch*cTeTmV8(0Yi-vD``0N;?(BR+tMyCT3{;6dpac{Ob%rs0 z_JzB#WoWOhtfte!_KCmZ-fAyamxjQCIM5cc?V@Z>WLJkxzlrjl}X-9f9~7$*|i9 zh@PZg4j5C^-9$(_AeO&-w}vn_q$bZ+*^N?Ln!|iB6C;m+y6Qg*&S#2cS2vTSXXnHi zQ@&D$+?)O(x;9?pTk;*wyL0P8-7hmVo$iQ$!N04?iBT_tTzeB2ZzrCB) zfYKoppZbd^N+xBAF&BSE7pMU1gy zR*n_)W=w8)Or;ThP2z%1-x!eg++r>MInmp!>`?Oy0PNWu^amHIW*o>n^A@+hcXhY$ z1i4aq!QE-*&)ARhHlDH_Z6M)fAoN zY~#mbWF9)Xf+G&8>7{b$2RA1&A?{7e{QHhp-mCp?#Es-H<6jrj%*v5tk2O)%66g!J zw+LQ~Rnw17TV#yDW&5Bc%OYxAU}feqSKhdeNSFT6uUkq+k*_0tAO^g1m*Z1u@JX@s z`hYM7kR?v?F)uBtcg+5oGB#---o+yA$;Ond;c;c+({QhUm>GwKn)+r{A6s!^EW$;q zu0_4Fp`|n-ftq5xnsi^ylUz=Bbj)18+YAO~#}@I3@n{`_HcfD!GmdJ-HAa2w5=)i_ zmr*;r4Q04z_hIyOGcdPGx4OdTI)9?j=ilV;9KTCo)(4E1-Dt?c57?>uNv1QXHw|o; zn}AsFKFt-amewBt`@O`Qf|8V-fWlzz*n(`wxod^h92PUi^4Hia6mp1_^w}RHt@HY$ z2{TF2$$cU~G0|Lo=jroLSlJ1@P#1O?v!x65?7>lLF~uz5b*N z$krZ-2-#6PG@$SmYxpRGBq$!&7{~BaZ+~B+i<01?L_ElcK_(^ zYuaYyjC$zw#y;J6ctcJLhID^yV%IUQ5J0^dScNUSdA|rvaadm;J*Sw?A-486>`xIkOF<~-W7DzT)UAbeX6S0KSxz{JQi=JLhwo#eQ+eu*5%c3}po`XE9 zWw7UxFyea9RamW>7M)S2i!6%&ejY@BXy^e{lQwtf%G57Z9Lss!hqa8@RG8{94dA*4 z3JD$T<>i>4ytiCvs6Bw7235`P)K7Dki{a#*(5fm2(e-O{54?mNW}Ikg@hIZ=TasPA z(^cgwGC+QMerDwc;#TsB&p=_LDo=iN_)(HMuU_=eiT(rOpOF~a_xr~DO~Ve~YgJ3} zF^Plm4V#>)hk2bUIaX3sDav`j0F=!wv^Xs^UX4ttt}O=G*#b&p@6BdOrHZg`)0W1T z5fofoXi~S!slLj-QQ2V8&F$Q(a(40D@YfijsB)fZX?$PbV0+YUAc+PQiwIy`lkZIH zBPPe5vWO;MN^;yI*1zs=x_!-lJ2!DN_1eoa#gF}PbrR)p zms`Bo1aEwkcl?acnP0;|h_4=d#Q_Oy+!jsR=nn5cUPsz%xj=MJ`~pc&+icR2hNdK? zr7nvq;W+UZ@jrTy)%uYjyt%5MD~^ZfZu5w;WhJ3BbTD1CvuegO=3$4YVX?n-Qy3e2 z`@?-?2pI`nm1!7zz(IPl4PRClI?# zVRxM#7MtLoZ>ur~FS*^7Wmrce)nSQ9oSL&-W=Mp*%k<+}|7`l`vmghU!dd(lvRp!?bP#$lp3K3R4`lboRfuS((340_Ei*;sX22wDU_e7LZDBhkK#POQu?|KtL^xf z&TERfo2!XvG^e$~C%)dtcmyQdq8|8OS9bK-<Mw3@y=FpSk&V4$A52NwKhv>iq_owZU|iY%QSR>xx$Sm%Ck9dT7oQIG%I z){%(XvMRarts^05%|7^o(OmAWOtGlK!Z88Enu5Nav>7u&eHO3BTuZxPZST-xhSKSj z)B*g^KiV$4h>%`o$A47K1|{-$DK1&V~GW_W~8o^PPN2uMTdKlA&YC?URh+% zkKncEp^DT9HD7Vb9J7tza{N8OlAed`t&F~HC;$4h_~UtuMy}58`urlX_nD#Ne|Qlt zM>!kAd`tzCR9*ZUmokLA)Lh`8tE6buJZ;=J&c~r z9~f=M;ud{<)OmDXArz@=8CQd`C?j7*`Ii)8Xdc>;6pLxm^NSd2{#HctSeONpE0^&iRpRwnmqWekL440}bQ z2;tEV?P+QL-*~K6pTB zc4-hCa^Hd5Gw$VkZCdW|5+g`K%0Ll86wi0VQ`7q-N<&S+5gv1`7n<-TmCHu-knQp0 zbK*B#+IwfNTJ&P6FP1(m--9!Ar#bY#H2|Oh)hMa-37@D4u(w9>@vu1e zwLFMeVGWq}kp6HtwX4pXp6&;E0wO=70E|gZB8o{;xc9M0yu+Z&{OQLK@gUg$)7yDR zHJxpH91AEQsF55 zkq*ib0wQ1mL}}{F-1XKx=DzW*d+)pNoxjd6XRUM2@0|17+4=47{$xtmQ!U#I?i_wNZLnhU&|!%rYi;SX;Pcl@BRg)X>a3=s-Lr%>h<%YfQ25km;0Z4$ z>A|?gpT_lPr#tw|)-*+;i-S3sQ_cX!+*JGWm?vk%4zr?(wsV6?0pci(Y3oz~^xsc~ZuDqnDlAi-_B9S+R89DiUN@*a_ zYiV}CkU8QYb>fw^Tk`@!2yW#+yWp-aSQcB!{moRse(ps5Pk>wtW7LtMNR>RDcB<%h zp~exM%D6!*0ulXL=-Qrhc>@Zub4Hl~G`5&PqgU&tr#@GHo=ns*l2%Z~1s%<;WNOfo zT1+NARA;1BRj2y)PMh{-RRU?=d^n)Qd>#OlkW^*TG_uAHeQ z;`1QYf!|ySNGoTZgpN)DRm_AoH6^r=Hnfr>9JjekC z-QA){vQOiH`2b(}+_A5hlX@1v1}64>=L(^s;H6(r3LZX>Rc;b}*zRw_u6R^7r`6LC zhR-#_+_DI$z}I4>bOpffS*|zXvnVRYQ(E;j0J)#bJUcM7<)N!>-D8d9s{q!$lUiFt z+nCmN0)rY!-@I|`f#0J54)(^9dHU^eS6Xh*5ovygH29XZ|H#nP;JoOzS#}M&T<_A3D`MPdE(t4}vVk+oho-EgN zNRCf$Qbj>0*|eF97u|H?BQ?Wa(Z|ngY1YQ}Vh|4}`@vFuuLGP=T{=IqQfEFZt?vRL zSNlTCghlYzO^Hv^MM4WlZvCtn_{yI-vZ?#&nHDIsPOI)5LfxnBspPHg>(ZfI64!@b z?d?qx%rAz~YlWU@^uJTeXLszGGtJs;oaJ*9uH-YuRu|%a^H(hV4S`z0mm1B+4dnjR z?x|eEJ`pkWjKqC9Efm>;tICb;e(JLkGUoQX#ocWP{{fxSpP^v0W21JHqs+pZ`zO7{ zO3HLo2F1;Z`h$Zww3ksd6V7pfJG)(_Rg_hBgU|R1cQC_ zShYO^jLjgwm3=y#sCJdG6`_5F;Kzwi5m-O1yGiH@r2$7rT7A{r0iNn&Qu&=^vbtPf z9VZ3r+W_VFgY)OINAm4Hy)OQ*Qr)j}JC(ffJ2RWXFgQ$Oe52)s|CeeMa>-}n=Ww(l@WVV&Iua0zpwp-w{bVUJKetY zxsI+6l4zv_-JBGEBZ7T-CJjKD8A~I(yXPW^r&AF4*OB7VqVzl^{vAaC6O-ST@8kqs zgO+hSVyIivhPWg4mlHfx+<(O~hSnnTDV5s|4cxmpiHY$GE1o0S7hY6Xr%+O&lF`+C zsjAseM2tL_#>{!miP|Prl4u?7WsW22A~KnnI)3NJY|{UE6@T=||1&65De>q1Pjh#g zf}Yt~GqjrJMNbt~6o@_XS)^l7eV>IkXd2gxGoVAJi52DM!%Z#p{v! zLniVaWh)q?N}&-)xGzJpjFzH0?A?NcXs*_Hj>rNvlkjoTF#(L5-bxJrmQAF!J3NZLpEh647X^Jtc{xfPYYWp5<3H#zGW4XB zG3ay85k)sbSxmuKbkQFx?JTa(lYlvon%ljB7YfP=QzO5ReDzPya zL;K1(vfsHx7Sl85dXc zuu6*()bWP7@Z$2*48a1~;7SxV8Gn>hj?B2G%n3>vUy8f3u3W6(nVSQW!>5DPp36bV z5sBBMqaXY?Vht`6F?z7^PP?8p!R|6|9Ar{WW85gX{sJIt3531L5Wm)oWg+EI7qQLY zqXm>Fq~pt~^2yS0H^It9q@YF>nOv3Xjm3tyLoZ!EymUqtOf`#Nl)w#<`>W)rNuX|j zj#H(gvJG4I*m!s4(?rXC`9z?)Pg($eyUdgmRR)5 z%c0f2lB9h2`Qpo|I20E0CF6stb$tC}buAXv6Gh8aMN!>vRqV8^jN4}^qT~CRN~^p- zr-00=9$!nAam{!43c3mUJxjTVOa{?w5N4e1^Zu(_IUwFuFWeMZlrHx+5#XgrlFIwe z#ZN4iN#f9VvlCMVG)4Vo(%~Iy(YbTBXNR2^z5Kinmq|gHsp~MdXnrzkq&>3!moI?( zpGIaB!yvb?WP^;!>ogLm)`}1ld+!SXP{wth{nf<(eV+*mH{DO_ zcMev%lB!8%~N?(HLFoGHI zWdi950`>GzYL9Yw2KpkRaF1og&U5|jhop?Bjw!(a#pCLE4~T8rR_L%>X_E*l`j;GY zROp8F6R^&YZIB?iMAZ9~!AYg(QSwNwl$S>aPhjjWMuIYpY@rlXD5B=YbTy&K|{?{k4(BcU@{M4pL??v8|26V$)yi41sS z+RKWa4N*gsyiAQVnuU!^(EIwchz;Q>bHv3gAf#3rsB)s8v0Z+h~6r&tFqZjaz(pJ zJh?V+GB}kz4=QKDk@b@?kJL)};N%z+cg{)}C+|{p9WeP&)K1(n=y+;*nUh!6@L%cQ zzwJ^({fz+l!zTDIZ`Bzk<+G)%w92ji`zS|0`071WPuvr5n=^dstJA#cms9}*@licZ z=2g^Uybpcr5i%K87A$?%`DI2v&PHRg*BpTq-XVwKWSDI=upQm~tbVe3Fo=U4{NbSg zXcG*cd3q^93K>-(oMl}eWp~mvKLh(SaJ}$Cj&ATM&_qaW^!SUKd+Md~EQgRUu^g-n z?VHoZo9BNu=qh?q+rq@KBnok*XGEcHO>3u&CVEqlm_}9uXPSX*KD2J*v zQ+BxFqh~=-OFQJ=i;iFP39Dm~;M!wPZNfduRIFuKKj+LEG5LUw)=xs_l$)s=K26-= zc_W#N>q47W{mW@gZ8TYT8D`NWL!CW)aiWLh&q5Fg4$uB2(7^wMC*YAi*5&ay!!}*L zjS)0~x!0_h7np^beA5C#lXYqBtjH*cJLsa(0?=_7COt zpEuxNxY}zoptD$!d;9RphnFeBRtgK5>-Garqc*<0?Gdo1i-d)f7JZM$b`0rmi!dG+ zRHe$>JIlnq?bGj0BoD~vmSt3Fm@K6iq{IDMppUG63g+5R%tV$yuh{WbBw#mP*xu`& zXq_=xw7w6Snrnfpu;PuUV=C1t4}LugW@sfKKx=A>FDR)RX%6lXPlam*KE-NK9fFQu zQj%K$eAUaJhMFrA^FP*tKv|Gihh`i1n^4Jjg0cIhMc!(j(X)g|AAGK;l;dPQK4ssd z8xgOoW|$ED0jNVLUv$GmZq$@cBKk2<+_cL~`#W$6M-c}=`I*q*6A zd;*24>I<89@D;1_LeS`i?2mXcaVmyKv|qxvZ3}_+G%9e)PA60%=Z@i&vfBL|pBAS@ zST{kcmDR>PhATI3nsytK(@`N-e$AF0)(0seJ#BQoZ#pdUd=b=H0 zF!fOlxatc$!kb)`cun!H;ov^`_J9;M$0j>+_NF~VuOznqkbcW-(YV$pDigI8adpar zkT4Fw*a^N>v7ASol_2aH&A3G8x#1eg>T3TuvbuBcb@SjB&f$f&KGGZK=@FecOlz*Z ziOfD!TGJi)C}q~&iKF|xpZ5x4YaTOd92v8zBk!BNu(JI4r;n=#CdyH$$qG++t;m{( z`toCR$uAGz@G6m^50~Y3TZWF=^Jjt-<*uqW4&i#X&Y4CAVGllbq?|lq|DrGlA(Ud3 zDXj|s&}-d(0}mj>p8YZn_nRArwH`XQQ&jSwDVu*B<^9Fb?_4SM?^gCoZj>J6fU1b! zxs-z@S^EuE9FI~)y^FR5o>_+w`xXN%-=|4xQlkvUZ?)^3X1FCL(q@u@j;jbx???_p3vR@sN6iM1U&NDk!FV#7AqGRlSK zdGAx-g>|4z$%VChtK8a(D<11fb0@!fbsDk3YiPdPO+1UeRwFHr93_o3DD}?r9l&6*pxM6^gAkAA>yvyw-bkay5qRjQ|@Szx)tE~*or`zwb#<$Byi?8n# zSwPE!^H_mj&MG(DsH~o$^%AO7eA2JQP-K5X(94tR{G?30^hJi?Q!VZL$~5)l-wUU* zuj7ra?&{nS;ciGOpXd`y!bvP3#hJE0rx4zte6UcQ3V!bP9>_s;FfV?aqwY{Po`i-%)F=sW813MjSE*971M7>UaJ$KgzP!=<7 zLp;85n{+GV*=z!VO3zh5MT?~|ei8hM{DiDC@`c}X20tgLe z7)NIU5C$={9wLYWAw6xpQZE~BtL8WJO>ZlJBZCk9Of;;0@bX+fE^*Ep*mBXHCIaS7 zX4U(yX-}F0bRao~;*Ow_#03g`EG{T*L&K5RK|4H&W6%{#YBJq>d%Os5gmE7 zBh@_7cH&7%BG{)f3O(I)&~Vw!ic1_~nfP+VfX_RF1guU6(42sC<4F0#a9{I+pizuf z?sqO(0DlCfWx{L&bq@}T;}07c6>QADYtqoLkY%17W6XyMNqKWNrBW=R_1-Mb%$gaj z##o;|7JoRmXg4!RY8&+@I`Ehmtjrjldd3{ zORY)#XSqo1%;Pi87+9xbwVir)ImvtdjRt?vnY;iDVJIMQBAI(W25zh$OD3a`9U3ZN zZ!}Glp)98oqI%9jqOEr*)-2FJuWylgPM`xn3Rq2e4tbb~`sI@7UQ|45#^~0oIxhIT z>)Nhs3U8O*s%AVraVtBuKRyVP(gwuH$EQ~U8(z4yZwNIX17{x$I>G&n6=EkU{FXhpfr?t?1%?N`6C*Gr?Yt``Ajas?RhSH?b51wc8 zRcxNlX?fvRoWDiRm8I7+Y^fjVO#lvZiWD$8a&<{ubC)6IL|N&ztBbiT9^P*@wtN2$ zRKC|H_jZp{@W$Q4JGK!%X{n5l>IO$B(e{|}q3k!TF5e(rCCar);*LsZmW;*jXYvuXP#i;u7f1Q8N^FD*L$g$qQeA^Pjw;Dqs!wD(sjXkWO-5BBtk? z_^#6KIpoP!Tw{32aSb>P?BJGR%Fjjh`wHDx=X=YqW%{K}%z?-=YBx{F13}4$k1G1r z;t7@gx}JT?y4lMVpvi$Zt+na#*`IY&wOdpGG_W>wpxGR*G4N4}t(J@9q04m#%{ZH>>_*T6tNFUDL3cvC$~?wRfyi&j^^rrALu96P~4?>siM}! z0r^-o9udEFWJjzdJEC$q;5QZc!&$XTFu8O1i5!(Oa{}XPyfWqQ=GHyV{jP23I8M{Q z)cXW!L@BRH%!*peq@g{?G@?90+!%LZ?~SG#19$e9J6E^Y**Q%Fz|H#bi>W_QQs7e6mt6y qZ{>cyp|1IzYvnd9Lc8cM2l($JQ@3^-=D+(M*)`h#t}6L`{67HwRj1$p literal 0 HcmV?d00001 diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio new file mode 100644 index 0000000000..a908f9a612 --- /dev/null +++ b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio @@ -0,0 +1,31 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg b/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg new file mode 100644 index 0000000000000000000000000000000000000000..b36fa27f4025e32f086de556210915f1a2f937f9 GIT binary patch literal 7550 zcmd5=cUV)~vflwjsz4}8v(Tgn(h{1AN;3&XLIRQmQ4A$O=tU6)K|q>H2pv?2F%S$$ zFA5ewil71kF?0nHlp+VPA}<`zIdH!Bo%g+a-~Hpw&fa^n*4ndXelvTm*|RpVHUUHPi+2q?!yd4}J{1Dkle3i-WAkF}zj)+hH`-jX0H7uY0Cuo8+7xa9fY444L}i{oNnIo#X;V37s@f{p+n`Vs*6u)p`QFaMz1Zg!UpTQ6Vs;SP8MuE1^p2KWGH z01Y;$4QK*d0Ca5-FabC@)@l99$tEstu65$!=H9~1%frXV%frjdCmBnpdVjGhGoMF9HsI7I+sVDLb>YpQzHkLq!=koy^(kU}OMdXNv-PMXyhGFJS&Tbm~9-=gb@VNxJc zNu6wJ*`E+%Z&*3*5KS0qb2Tb>D)>3VH!P5Y&Vg<*Qj^8_6+f<=$LrHv&lFpWpM~aq zOeh4>{H;4$?Q>NZh(@ossk}Zh(;IVAkak{<4k+U6%FFs_d=I3pS4=hurbqHRh<&^p zOn6et-P>^eO;FEH%CLl{@BQ!Rdo#stRXak>lBDN;jx447ES;?3Q>z+kJk2nt+LpaXzO&3AJUaJve;p`I|HD-k3bLOnS;%x-Cuk(R zJg@r<_xFc24F-{$%-pjH7xZDS;!S35!bSWzNOhB$G8?#bL`oqUC98*vY) z-uf$MI2{(-(=DrCEe^(rv*w&N`zgr6fhCndB}C=efgc$|ksZ0gtzz9pUdSY-r_MS_ zA69gd&LK=Fu$cQ9Vi~XD)rXu*)g*+rBA20?NU4)s%YY;juYm5E%`y9`TG z57xg)ovOIC+|7Bez2&1Bg?S2F6d!o0edN-Yk^g_wJVb1W@(f$2Sz6nS~#K}1+oog;?^$eL@Dknbpktt|GuqF~A zwW*4#3dMwDl7^qYEhYz=+*94*YUMVS<|ixbUGNq;4t@Lx*FUjvl@DQ?V^yT;8-!I; z=Y?A*YSsYJ6rD6><}0o&dXVJvDXlfhtx>@VHc*G1I7MkzG*3z>`0WUkq)*ZO(1V*h|4S;DZ-n2 z!Lm{+lT&+rHdgIO@%6lro!u1=?BNLRyCUAvck$Iz-m4}L)RN2mWq*DnPEg zyI(hK-wj*o9Os&RHP?uqfb4Vyhk0f6J}=rUFJ`=$fqk~}QaZil4&Pgps7O0ch_-}f zyWUy5WU5a-!u(@$Lo}%R@bBsY9O%vKMc3{GGX{!0u52^E`G`U zenG!goB!(+{}aJg7XSickYqvlPlFdPTiJw#pL&0b9>P`v%K@+g~u&)StnxeT&PNA$Sfj^;V&wn z$1PuM(h+T=)f)$Rh(2U8$r`@Sf$lJd>dOZrZ1lFNs;ZzE4N{YzBBjk?EONz?rER<)YJrgPt5_U z^0ex1F}*D0_?SK3DcCU4%6_}V?TSRyunx#huHK8FPMx)hK7^S=k{oL);exrKlD=n) z)EJ3=IhMey4^n%j^iOXxM5pGDD%$KNWHSGk;Q7Dj4EnqV}lxd2nl- zI0j-E?B?XspQ4l{`8_?uP-a??6f)kR7$5Hm%g({#sryJ?NC|wHcejz zg1P8t_A}jU5h)7Y>J#80-ITp{3K`l+*!~GqHi`MIBL&)&eQrUq^D3RKr@I3NW5ft# z0eFBZ|IQf6zUC%1k{usrw|1JeuMWt{F!|UL))Og)k+N)Sdqe~Tjhk_9Es0TUK%M(I z)k6FfHps|r3p$p9WuDbK{eb31o$^fa((1Jz-o*{ecB%G}CP1L6kXwB?cP+nXm+Rz4 z5GkjJrfV`(;@$9XBj74iDm>7(rI#zb6~?Qx5iE{2&XZmzo+XzTLY;h|vUbWgxEeu& z`tTr};4>F0ho!?10x63^;w+FJM{2DqrxhxPYo})w9>|z=Dt9_!sVjVr+8d+T^o&c##ojOL`Eg0DJ0NY3m8+Uy5c{o@yO?4TX zCk0^zrF$+&lAB|EbJ2SmIX;*d(v^B*q+`C$3mPh1`)b!I8$z>7npDv)oE1Ns-ZU$H z7lt1|2Uu>els}cLs4mjkxzc%sY)VoTVH_#D1xYaXnEN7R(O3-i-C9M5HdT4bLb<3f zQjvNz(`$mQq#>u@w*6cKCY~wEo8C<}>Pvrop4s^VSD{>~V&@l9Y*WOX5q$$oR7t1| zKxoM=P#=oZrWsx7aBnhsj~2Mf5X&nsuLwMh-?U*vwu2s`YG!tn?gjkoTM9c%%^Ai= z<4@Kom$M9fpffp&ZPWueRfG4@$hIr}sXFom>AiP`|9g(f!EbpB(cJFP@EOxwe07+P zO>1B3u;D6!Ct4R&2w%BAk$Eh*wrAz*sAK!lWs}RM1enC7Fi^4X`_y^M3k@#z>OZix zV~_442NLb8=ckHLa4$IRX|U;pE}Bw=_rl~JyfRM&w^cb9B6{MI+X6M={^DLmL3>p{ zRKQYiF|S_EOD7T1?LHsizZeK>YyEzQ!h-8ED?#Ov>!Hl95-gSgfHC~sMnX&948nS% z%=x@_cE;@W;UdguE^Bei;+7Dxr+NwI%Nbw-CgeK)_DrfaGb!m|TkBAw_f!t!t>cIQalHaDkvEs+%LS|KzV!VAi zySSp@Fe4S1ged@MVdn+zemv$T?|_0wrE$Hg4ZCTdVHJM8T+W{oqQZQ0xWsl*)- zfT@(Om+{yxuuY=bpqp+<39DYgw+3sJHyp>imsj3iI&`MjL|)@mF{@H));B=v zbGuGEdv2L9bfDV4Bdx$P9#j3Mx8TaNn@$iptq%at^6RuA2;*f*LNK@d(z%)g4sUYi zEHkuqxf*AjBBD(EXFHL>1Vw#IMMlNTzM>R??4idpdR3#Bpg9)VOEbYR)_omX-@E7J zA|DI=8UNM^!x~vRS92D!N=4cFGRZpTP6)8~rJpG8n8v+347=d^iBOkgF6g7E*d3?) zW^0-DPX1O+M1-7Ufgx5NiKM6_&7F^&^L)JA{kFT$^zItqPX6(tP`nGJn)CbsnffLy z|B1fcdyFtkZ18FkclscV=E^Hq2ng^j?B};`9Bx|aXn&fi{5}%RYle_hvWjx`MI%h05VExiVX>`S3)<;St|Dz&yVCvWtSq8B{2+g3)ypf1nPHDO zh!JDx;`q=Ojk$W~?CK(Nd=U9*oVMk5`-~CSmf2%Tzj;B)mSFq#nK+(j9!ZHN%X`P3 zOEF8}#8+~IuXEr&M*b`peC(b=%8jzFfn= zfMvfWRzS@>A0DT7*%5Cr_JAiFCt^vgDhzlqUSVGsLC!Wih6^}F4i{=tm9)@DNopAH z)P0|;>V(7<*~qzlyq)vn!A#x-FC~on+XQ6WbrSqa;*sf=Ch2YBE?LelgICdf2Y1YV z@nv{9*4P|OKB0|FN_Vcl5iC;tt!@oa^dbYiRYDq>#=e^VMb*uz9@M7v4t)P!_!v$6 zO_+|>=ND?xt;8paN=Ddy8H)qGnXXJV=x{Z?k2NeIS~fXE>NdRXuF{u3)zgF73uZAr zyjO&y4n|q`w@c21za0cXkjI^MWA8XkulGy6PC51bhNqKx=^l6*vQQn)Lf#}#7rlbm zW>;Hb72Lu^_>KdcKIb{;n?K0uk?gvr+HBbNVdF5rUGq0-tNSm{JFEeS2O~Z!kb$3# z7lK~>sOrr;vur8TRNv4zT%i=dCo^TLjcy($4oAUK6dT_ro_nWQ{syl}%_&LA@!9(c zld`(ET<16_wnsBs$iv$<^U_hj=h4Rl7$Vc6w~t*2Oz(M(%NPl6F;M9xw(LFoExjb* zV6dF_N&zN_XZu0(#W-FoG`*YBoc-z0yJubZyr5OSULkPnPp;K4MM+7KtQ3*$_kaWZ z=1rB}(3xb6E>z_T12uZrMk(3iVdkfl`srE8_nt575|8d*l-o6z>WXDb1s_T^zosf< zh<#x!o9^BQ4;hAJuPiywrQ{TA!&gWa`6(h)rITa8Z-h!7UFyBsQf9jU8zr#572Glk z+7p&in1_k?3H+^|fzy5mkrX<%zC3bm4$!|9*)Dv4v47xn1dil$pCo?4ZmP-crh%|e z_FbL|imsO~L}?#Ey=>2}`f*A97;wCsMbXaasq-9~W#6C8w-RY+^tfQB!YbU+M1|+7 zKk1Xn$bw6tAH}=hYF5RNZM;O*7a(`A?)(!32BG7zGDNzl`%YCPH`O6W`K|ip+H@)R z@WmS2LBw;CJjInfd!vIVybrhK3B60n3LISh)ht7Hpu|Ttb%$S0fV05KCPsZ)K5lpX z6C?@_OTUcAJ&6RA!g2SgD9MoT3qC45IZ((E*5$Ra%3j=dFrm+|Z&*o+!iX9#N0)me0aa_1g!i5HO?ADb}K+) ztMMmvXxSOI#cfC`iq4O$CetPjJ%hVYZj4m>cF7x;O=dPSkiWkce1+>C1|Io@^EIhG z84H;#>2}w!q!?vUF!}uB{VCr_PI{z)!?V2Cq0dJFgTVV5UkAs4nOob?i&G&^ztue2hMRlV z81e-$EaXfJuN%$?pIzYmSA}g_iZ~DdF^Aw9u(4Zhu2KK}9cvTVyXtBj^Tp9^{O0yu zMXOZb-a?$--0BOyv9cWZ^Y_Q#1FYd$?^!jgAm$QttMj9PKTQqzr9Y_euuSnErpo-% z9|%6aRrTvHQ@8#BhAaxy(fG?$&>vuIMFan)FzGd5a~)ul`M>IhzufxwV!;Hr=+E+- zPk!vH@OzPXjrp^uW}2xX{rTcljNgf_iiY6@MQ@_dN_9xuoqEqOPwhW+{Xeb7I4B7ilYL53Te4M(=+1" --loglevel INFO` + example `java -jar theta-xsts-cli.jar CEGAR --model crossroad.xsts --property "x>1" --loglevel INFO` runs the default analysis with logging on the `crossroad.xsts` model file with the property `x>1`. @@ -55,40 +56,48 @@ residing on the host: Note that the model must be given as the first positional argument (without `--model`). -## Arguments - -All arguments are optional, except `--model` and `--property`. - -* `--model`: Path of the input XSTS model (mandatory). Can also accept PNML files with the `*.pnml` - extension. -* `--property`: Input property as a string or a file (*.prop) (mandatory). For PNML models an unsafe - target marking can also be described by listing the values of each place in their order of - definition separated with spaces. -* `--cex`: Output file where the counterexample is written (if the result is unsafe). If the - argument is not given (default) the counterexample is not printed. Use `CON` (Windows) - or `/dev/stdout` (Linux) as argument to print to the standard output. -* `--loglevel`: Detailedness of logging. - * Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` ( - default), `INFO`, `DETAIL`, `VERBOSE`. -* `--version`: Print version info (in this case `--model` and `--property` is of course not - required). -* `--metrics`: Print metrics about the XSTS model (number of variables and statements). -* `--initialmarking`: Can be used with the PNML frontend. Override the initial markings of the - places. Format: list the values to be assigned to each place in the order of their definition in - the PNML file separated with spaces. -* `--visualize`: Visualize the result of the analysis (the reachability graph if the model is safe, - or a counterexample trace if it is unsafe). Prints to the dotfile given as parameter. -* `--optimizestmts`: The algorithm can optimize stmts by detecting failing assumptions and - unreachable branches of choices. - * Possible values: `ON` (default), `OFF`. - -The arguments related to the algorithm are described in more detail (along with best practices) -in [CEGAR-algorithms.md](../../../doc/CEGAR-algorithms.md). - -### For developer usage - -| Flag | Description | -|----------------|-----------------------------------------------------| -| `--stacktrace` | Print full stack trace for exceptions. | -| `--benchmark` | Benchmark mode, only print metrics in csv format. | -| `--header` | Print the header for the benchmark mode csv format. | +## Subcommands +There are two categories of subcommands, one for model checking and one for helper texts. For up to date information, run the +CLI without any subcommand, or with the `--help` flag and the available subcommands will be printed for you. +### Algorithms +The following subcommands are available as arguments: + +| **Feature** | **Description** | +|---------------------|----------------------------------------------------------------------------------------------------------------------------------| +| **CEGAR** | Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm | +| **LTLCEGAR** | Model checking using the CEGAR algorithm with an LTL property | +| **BOUNDED** | Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use `--variant` to select the algorithm (by default, BMC is selected). | +| **MDD** | Model checking of XSTS using MDDs (Multi-value Decision Diagrams) | +| **PN_MDD** | Model checking of Petri nets using MDDs (Multi-value Decision Diagrams) | +| **CHC** | Model checking using the Horn solving backend | + +### Helper commands +There are two subcommands that simply output information: + +* **header** : Used to print a header for outputs generated by the `--benchmark` option in the algorithm commands. If you are doing +a larger benchmark with multiple runs piping into a file, this can be run first to provide a header for the file +* **metrics** : Prints information about the input xsts model + +## Common arguments + +There is two group of arguments that are mostly common among all the algorithm subcommands. + +### Input options +Options related to model and property input + +| **Option** | **Description** | +|----------------------------|-------------------------------------------------------------------------------------------------------------| +| `--model=` | Path of the input model (XSTS or Pnml). Extension should be `.pnml` to be handled as Petri-net input | +| `--property=` | Path of the property file. Has priority over `--inlineProperty` | +| `--inline-property=` | Input property as a string. Ignored if `--property` is defined | + +### Output options +Options related to output and statistics + +| **Option** | **Description** | +|------------------------|--------------------------------------------------------------------------------------------------------| +| `--log-level=` | Detailedness of logging. Possible values: `RESULT`, `MAINSTEP`, `SUBSTEP`, `INFO`, `DETAIL`, `VERBOSE` | +| `--benchmark=` | Quiet mode, output will be just the result metrics. Possible values: `true`, `false` | +| `--cexfile=` | Write concrete counterexample to a file | +| `--stacktrace` | Print stack trace of exceptions | +| `--visualize=` | Write proof or counterexample to file in DOT format |