{"header":{"message":"WIP","description":null,"timestamp":"2023-06-01T07:53:47.471600139Z","authors":[{}]},"hash":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC","authors":[{"login":"paradyx","key":"6haf2odGMeVaBH1hYPXKBZAYaktbbMcbxkvUdyZKMhVc"}],"deps":{"hashes":[["6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC","WIP"],["AA",null],["RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC","More stochastic"],["KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","WIP"],["DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC","some more theory"],["QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","WIP"],["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","Initial"],["EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","WIP"],["B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","WIP"],["UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","WIP"],["X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC","WIP"],["JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC","WIP"],["MQJMCLGFSBSFJ3JPCIHQSBZS4XZPGJI7NGGRASX5UVGJO6HES25AC","More background, better acronyms"]],"deps":["RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC"],"known":["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC"]},"hunks":[{"Replacement":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":5,"ins":{"up_context":[{"change":3,"pos":133}],"down_context":[{"change":3,"pos":184}],"flag":"BLOCK","start":0,"end":51,"inode":{"change":3,"pos":35}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":133},"to":{"change":3,"start":0,"end":51},"introduced_by":3}],"inode":{"change":3,"pos":35}},"ins_contents":[{"Add":{"text":"\\LoadClass[a4paper,12pt,twoside,openright]{memoir}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:50"}}],"del_contents":[{"Del":{"text":"\\LoadClass[a4paper,11pt,twoside,openright]{memoir}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:50"}}]}},{"Replacement":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":17,"ins":{"up_context":[{"change":3,"pos":406}],"down_context":[{"change":3,"pos":448}],"flag":"BLOCK","start":52,"end":94,"inode":{"change":3,"pos":35}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":406},"to":{"change":3,"start":406,"end":448},"introduced_by":3}],"inode":{"change":3,"pos":35}},"ins_contents":[{"Add":{"text":"\\settypeblocksize{700pt}{1.2\\lxvchars}{*}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:93"}}],"del_contents":[{"Del":{"text":"\\settypeblocksize{600pt}{1.1\\lxvchars}{*}","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:447"}}]}},{"Replacement":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":19,"ins":{"up_context":[{"change":3,"pos":473}],"down_context":[{"change":3,"pos":498}],"flag":"BLOCK","start":95,"end":120,"inode":{"change":3,"pos":35}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":473},"to":{"change":3,"start":473,"end":498},"introduced_by":3}],"inode":{"change":3,"pos":35}},"ins_contents":[{"Add":{"text":"\\setulmargins{3cm}{*}{*}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:119"}}],"del_contents":[{"Del":{"text":"\\setulmargins{4cm}{*}{*}","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:497"}}]}},{"Edit":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":30,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":756},"to":{"change":3,"start":756,"end":757},"introduced_by":3}],"inode":{"change":3,"pos":35}}},"contents":[{"Del":{"text":"","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:756"}}]}},{"Edit":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":127,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":3103}],"down_context":[{"change":3,"pos":3103}],"flag":"BLOCK","start":121,"end":184,"inode":{"change":3,"pos":35}}},"contents":[{"Add":{"text":"% Section reference","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:140"}},{"Add":{"text":"\\renewcommand*{\\sectionrefname}{Section~}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:182"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:183"}}]}},{"Edit":{"inode":{"change":3,"pos":6845},"path":"main.tex","line":36,"atom":{"NewVertex":{"up_context":[{"change":11,"pos":223}],"down_context":[{"change":11,"pos":223}],"flag":"BLOCK","start":185,"end":206,"inode":{"change":3,"pos":6845}}},"contents":[{"Add":{"text":"\\usepackage{optidef}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:205"}}]}},{"Edit":{"inode":{"change":12,"pos":18034},"path":"literature.bib","line":641,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":5399}],"down_context":[{"change":2,"pos":5399}],"flag":"BLOCK","start":207,"end":278,"inode":{"change":12,"pos":18034}}},"contents":[{"Add":{"text":" file = {:/home/paradyx/MA/literatur/truchet2010synacs.pdf:PDF},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:277"}}]}},{"Edit":{"inode":{"change":12,"pos":18034},"path":"literature.bib","line":647,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":5551}],"down_context":[{"change":12,"pos":35999}],"flag":"BLOCK","start":279,"end":1155,"inode":{"change":12,"pos":18034}}},"contents":[{"Add":{"text":"@InCollection{karp2010reducibility,","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:314"}},{"Add":{"text":" author = {Richard M. Karp},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:347"}},{"Add":{"text":" booktitle = {50 Years of Integer Programming 1958-2008 - From the Early Years to the State-of-the-Art},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:453"}},{"Add":{"text":" publisher = {Springer},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:479"}},{"Add":{"text":" title = {Reducibility Among Combinatorial Problems},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:538"}},{"Add":{"text":" year = {2010},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:560"}},{"Add":{"text":" editor = {Michael J{\\\"{u}}nger and Thomas M. Liebling and Denis Naddef and George L. Nemhauser and William R. Pulleyblank and Gerhard Reinelt and Giovanni Rinaldi and Laurence A. Wolsey},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:753"}},{"Add":{"text":" pages = {219--241},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:779"}},{"Add":{"text":" bibsource = {dblp computer science bibliography, https://dblp.org},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:849"}},{"Add":{"text":" biburl = {https://dblp.org/rec/books/daglib/p/Karp10.bib},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:913"}},{"Add":{"text":" doi = {10.1007/978-3-540-68279-0_8},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:958"}},{"Add":{"text":" file = {Old Book:/home/paradyx/MA/literatur/karp1972reducibility.pdf:PDF},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1040"}},{"Add":{"text":" timestamp = {Wed, 14 Nov 2018 10:12:21 +0100},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1089"}},{"Add":{"text":" url = {https://doi.org/10.1007/978-3-540-68279-0\\_8},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1151"}},{"Add":{"text":"}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1153"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1154"}}]}},{"FileAdd":{"meta":{"basename":"ch3_example4.tex","metadata":0},"context":[{"change":3,"pos":7550}],"contents":[{"Add":{"text":"% TeX root = ../main.tex","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1222"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1223"}},{"Add":{"text":"\\todo{unfinished}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1241"}},{"Add":{"text":"\\begin{tikzpicture}[program]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1270"}},{"Add":{"text":" \\node[state,initial] (l0) {$l_0$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1332"}},{"Add":{"text":" \\node[state] (l1) [below=of l0] {$l_1$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1394"}},{"Add":{"text":" \\node[state] (l2) [right=of l1] {$l_2$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1456"}},{"Add":{"text":" \\node[state] (l3) [right=of l2] {$l_3$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1518"}},{"Add":{"text":" \\node[state] (l4) [below=of l1] {$l_4$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1580"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1581"}},{"Add":{"text":" \\path[->] (l0) edge node[swap] {$\\textit{true}$} (l1)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1649"}},{"Add":{"text":" (l1) edge node[swap] {$x > 0$} (l2)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1717"}},{"Add":{"text":" edge node[swap] {$x \\leq 0$} (l4)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1785"}},{"Add":{"text":" (l2) edge node[swap] {$y > 0$} (l3)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1853"}},{"Add":{"text":" edge node[swap] { \\begin{aligned}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1915"}},{"Add":{"text":" y &\\leq 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:1977"}},{"Add":{"text":" x &:= x-1 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2039"}},{"Add":{"text":" z &:= z+2 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2101"}},{"Add":{"text":" \\end{aligned}} (l1)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2169"}},{"Add":{"text":" (l3) edge node[swap] { \\begin{aligned}%","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2232"}},{"Add":{"text":" x &:= x+y \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2294"}},{"Add":{"text":" y &:= y-1","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2353"}},{"Add":{"text":" \\end{aligned}} (l3);","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2422"}},{"Add":{"text":"\\end{tikzpicture}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2440"}}]}},{"FileAdd":{"meta":{"basename":"ch3_example3.tex","metadata":0},"context":[{"change":3,"pos":7550}],"contents":[{"Add":{"text":"% TeX root = ../main.tex","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2508"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2509"}},{"Add":{"text":"\\begin{tikzpicture}[program]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2538"}},{"Add":{"text":" \\node[state,initial] (l0) {$l_0$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2600"}},{"Add":{"text":" \\node[state] (l1) [below=of l0] {$l_1$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2662"}},{"Add":{"text":" \\node[state] (l2) [right=of l1] {$l_2$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2724"}},{"Add":{"text":" \\node[state] (l3) [right=of l2] {$l_3$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2786"}},{"Add":{"text":" \\node[state] (l4) [below=of l1] {$l_4$};","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2848"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2849"}},{"Add":{"text":" \\path[->] (l0) edge node[swap] {$\\textit{true}$} (l1)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2917"}},{"Add":{"text":" (l1) edge node[swap] {$x > 0$} (l2)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:2985"}},{"Add":{"text":" edge node[swap] {$x \\leq 0$} (l4)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3053"}},{"Add":{"text":" (l2) edge node[swap] {$y > 0$} (l3)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3121"}},{"Add":{"text":" edge node[swap] { \\begin{aligned}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3183"}},{"Add":{"text":" y &\\leq 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3245"}},{"Add":{"text":" x &:= x-1 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3307"}},{"Add":{"text":" z &:= z+2 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3369"}},{"Add":{"text":" \\end{aligned}} (l1)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3437"}},{"Add":{"text":" (l3) edge node[swap] { \\begin{aligned}%","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3500"}},{"Add":{"text":" x &:= x+y \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3562"}},{"Add":{"text":" y &:= y-1","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3621"}},{"Add":{"text":" \\end{aligned}} (l3);","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3690"}},{"Add":{"text":"\\end{tikzpicture}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3708"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":141,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":862}],"down_context":[{"change":3,"pos":862}],"flag":"BLOCK","start":3710,"end":4125,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"Selecting the locations to abstract is crucial for good implementation. From a","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3788"}},{"Add":{"text":"theoretical point of view the selection of locations to abstract guarantees","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3864"}},{"Add":{"text":"termination of the control-flow refinement. Yet, with every abstraction the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:3940"}},{"Add":{"text":"refined program looses precision compared to the evaluated control-flow. In the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4020"}},{"Add":{"text":"following some different possibilities to select the locations marked for","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4094"}},{"Add":{"text":"abstractions are discussed. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4123"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4124"}}]}},{"Replacement":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":157,"ins":{"up_context":[{"change":3,"pos":1083}],"down_context":[{"change":3,"pos":5065}],"flag":"BLOCK","start":4126,"end":8903,"inode":{"change":3,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1083},"to":{"change":3,"start":1083,"end":1475},"introduced_by":3}],"inode":{"change":3,"pos":7949}},"ins_contents":[{"Add":{"text":"The naive solution would be to just abstract at every location, as it also stated","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4207"}},{"Add":{"text":"in \\cite{Domenech19}. The advantage is that the implementation is easy, and the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4287"}},{"Add":{"text":"resulting program and analysis thereof quick. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4334"}},{"Add":{"text":"The disadvantage is that a lot of evaluated control-flow is lost to the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4406"}},{"Add":{"text":"abstraction. Every abstraction requires $\\Theta(n)$ calls to the SMT-solver","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4482"}},{"Add":{"text":"which is computationally expensive. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4519"}},{"Add":{"text":"In addition control-flow refinement was introduced to unroll loops in such a way","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4600"}},{"Add":{"text":"that hidden branching is resolved. The heuristics presented by \\cite{Domenech19}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4681"}},{"Add":{"text":"are focused on loops and the properties are selected for the loop heads.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4754"}},{"Add":{"text":"Constructing a heuristic, that is well suited for every location in the program","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4834"}},{"Add":{"text":"is not obvious is left open for future work. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4880"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4881"}},{"Add":{"text":"\\subsection{Abstract Loop heads}\\label{ssec:loopheads}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:4936"}},{"Add":{"text":"The second method proposed by \\cite{Domenech19} is to abstract only on loop","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5012"}},{"Add":{"text":"heads. Termination is guaranteed since every infinite path in the evaluation","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5089"}},{"Add":{"text":"tree of a finite program must visit some loop (and in turn the head) an infinite","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5170"}},{"Add":{"text":"number of times. With only finitely many abstraction candidates (versions), it","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5249"}},{"Add":{"text":"is guaranteed that at some point some version repeats and the evaluation","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5322"}},{"Add":{"text":"backtracks. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5335"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5336"}},{"Add":{"text":"The exact definition of a loop head is unclear. For sake of termination it is","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5414"}},{"Add":{"text":"sufficient that every loop contains at least one (but possibly arbitrary)","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5488"}},{"Add":{"text":"location marked for abstraction. The intuitive candidate is the head of the loop","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5569"}},{"Add":{"text":"since that's the location where most branching will probably occure in practice.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5650"}},{"Add":{"text":"For this implementation a loop head is defined as follows.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5709"}},{"Add":{"text":"\\begin{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5728"}},{"Add":{"text":" A \\textit{loop head} are the entrance locations to a loop encountered during","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5809"}},{"Add":{"text":" a depth-first search starting at the start location $l_0$. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5873"}},{"Add":{"text":"\\end{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5890"}},{"Add":{"text":"A loop can have multiple loop heads, when it can be entered from different","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:5965"}},{"Add":{"text":"locations, or when overlapping with other loops (see examples \\todo{} \\todo{}).","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6045"}},{"Add":{"text":"Detecting loops and loop-heads is further discussed in \\Sref{sec:findingloops}.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6125"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6126"}},{"Add":{"text":"\\todo{prove upper bound on program size}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6167"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6168"}},{"Add":{"text":"\\subsection{Feedback Vertex Set}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6201"}},{"Add":{"text":"As stated in the previous section \\Sref{ssec:loopheads}, it is sufficient to","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6278"}},{"Add":{"text":"find only a set of locations that cover every loop in the program. The problem","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6357"}},{"Add":{"text":"is one of Karp's 21 NP-complete problems and","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6402"}},{"Add":{"text":"commonly called \\textit{Feedback Vertex Set} or \\textit{Feedback Node Set}\\cite{karp2010reducibility}. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6506"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6507"}},{"Add":{"text":"\\begin{definition}[Feedback Vertex Set Problem]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6555"}},{"Add":{"text":" Given a directed graph $G = (V, E)$. Find the minimal subset $R \\subseteq","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6633"}},{"Add":{"text":" V$ such that every (directed) cycle of $G$ contains a node in $R$.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6704"}},{"Add":{"text":"\\end{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6721"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6722"}},{"Add":{"text":"Detecting all loops(cycles) in a graph is easily done by \\gls{dfs} on the graph.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6803"}},{"Add":{"text":"And the problem can instead be formulated as a hitting set problem. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6872"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6873"}},{"Add":{"text":"\\begin{definition}[Hitting Set Problem]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6913"}},{"Add":{"text":" Given a finite collection of finite sets $S = \\{S_1, \\dots, S_n\\}$, where","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:6991"}},{"Add":{"text":" each $S_i \\subseteq U$ for some set $U$, find a minimal set $R$ such that","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7069"}},{"Add":{"text":" $R\\intersect S_i \\neq \\emptyset$ for all $i = 1,\\dots,n$.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7131"}},{"Add":{"text":"\\end{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7148"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7149"}},{"Add":{"text":"A hitting set problem can be formulated as a \\gls{lip} and solved by readily","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7226"}},{"Add":{"text":"available \\gls{smt} solvers. Recall definition \\ref{def:loop}. In the following","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7306"}},{"Add":{"text":"the \\gls{lip} used for finding the feedback vertex set of an integer program","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7383"}},{"Add":{"text":"with locations $L$ and a total of $N$ loops $a_1, \\dots, a_N$ is constructed. It","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7464"}},{"Add":{"text":"is assumed that all loops have been found by \\gls{dfs} as described in","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7535"}},{"Add":{"text":"\\Sref{findingloops}.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7556"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7557"}},{"Add":{"text":"\\begin{mini!}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7571"}},{"Add":{"text":" {}{\\sum_{i=1}^{n} x_i\\label{eq:lip1-goal}}{\\label{eq:lip-vfs}}{}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7640"}},{"Add":{"text":" \\addConstraint{\\sum_{i : l_i \\in \\text{Loc}(a_j)} x_i}{\\geq","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7704"}},{"Add":{"text":" 0,\\protect\\quad\\label{eq:lip1-hit}}{j = 1,\\dots,N}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7759"}},{"Add":{"text":" \\addConstraint{ x_i }{\\leq 1,\\protect\\quad\\label{eq:lip1-leq1}}{i = 1,\\dots,n}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7842"}},{"Add":{"text":" \\addConstraint{ x_i }{\\geq 0,\\protect\\quad\\label{eq:lip1-geq0}}{i = 1,\\dots,n}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7925"}},{"Add":{"text":"\\end{mini!}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7937"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:7938"}},{"Add":{"text":"Every variable $x_i$ of the \\gls{lip} \\ref{eq:lip-vfs} indicates if a location","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8017"}},{"Add":{"text":"is part of the hitting set in which case the variable is assigned to 1, or not","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8096"}},{"Add":{"text":"in which case the variable is assigned the value 0. The constraints","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8164"}},{"Add":{"text":"\\ref{eq:lip1-hit} guarantees that every loop is \\enquote{hit}, while","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8233"}},{"Add":{"text":"\\ref{eq:lip1-leq1} and \\ref{eq:lip1-geq0} enforce that every location is only","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8311"}},{"Add":{"text":"selected at most once. The optimization goal \\ref{eq:lip-vfs} being to select","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8389"}},{"Add":{"text":"the fewest locations possible.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8420"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8421"}},{"Add":{"text":"Computing the feedback vertex set of a program is independent of the partial","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8498"}},{"Add":{"text":"evaluation and can be done a-priori. It is thus considered to be an offline","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8574"}},{"Add":{"text":"method. It shall be noted that the locations inside the feedback vertex set do","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8653"}},{"Add":{"text":"not need to be the closed location to the start location of a loop. For","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8725"}},{"Add":{"text":"determination of properties it might be necessary to rotate the loop so that the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8806"}},{"Add":{"text":"marked locations are the first location in the loop. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8860"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8861"}},{"Add":{"text":"\\todo{prove upper bound on program size}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8902"}}],"del_contents":[{"Del":{"text":"\\subsection{Abstract Loop heads}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1115"}},{"Del":{"text":"\\begin{comment}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1131"}},{"Del":{"text":" technique: ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1147"}},{"Del":{"text":" - offline","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1161"}},{"Del":{"text":" - daikstra","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1176"}},{"Del":{"text":" - FVS","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1186"}},{"Del":{"text":" pro: ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1196"}},{"Del":{"text":" - probably close to optimal","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1228"}},{"Del":{"text":" - heuristic from domenech19","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1260"}},{"Del":{"text":" - unclear how to propagate for overlapping loops.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1314"}},{"Del":{"text":" contra:","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1326"}},{"Del":{"text":" - fvs is NP-complete [citation needed]","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1369"}},{"Del":{"text":" - possibly cheaper for scc instead of whole program","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1425"}},{"Del":{"text":" - unclear what a loop-head is.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1460"}},{"Del":{"text":"\\end{comment}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:1474"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":245,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1504}],"down_context":[{"change":3,"pos":1504}],"flag":"BLOCK","start":8904,"end":9651,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"We have seen two offline strategies to select locations for abstraction. In the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:8983"}},{"Add":{"text":"following we will introduce a technique that decides on abstraction during","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9058"}},{"Add":{"text":"partial evaluation using the path evaluated. The technique counts the number of","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9138"}},{"Add":{"text":"occurences on the path for every location in the program. Instead of abstracting","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9219"}},{"Add":{"text":"on first re-occurrence, one can decide on a parameter $k \\in \\N$ resulting in","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9297"}},{"Add":{"text":"the first $k$ re-occurrences to be ignored before abstracting.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9360"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9361"}},{"Add":{"text":"The idea is to unroll loops up to a constant number of times so that loops with","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9441"}},{"Add":{"text":"constant bounds $b \\leq k$ are perfectly unrolled without any abstraction. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9517"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9518"}},{"Add":{"text":"\\begin{example}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9534"}},{"Add":{"text":" \\todo{example with constantly bounded loop}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9582"}},{"Add":{"text":"\\end{example}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9596"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9597"}},{"Add":{"text":"\\todo{formalize, prove upper bound on program size}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9649"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9650"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":272,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1784}],"down_context":[{"change":3,"pos":1784}],"flag":"BLOCK","start":9652,"end":9653,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9652"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":274,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1821}],"down_context":[{"change":3,"pos":1821}],"flag":"BLOCK","start":9654,"end":10289,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"During this section the fact that programs are probabilistic has been completely","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9734"}},{"Add":{"text":"ignored. One could wonder if loops with zero probability should be removed in","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9812"}},{"Add":{"text":"order to further shrink the problem. We will assume that all transitions with","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9890"}},{"Add":{"text":"zero probability have been removed before the analysis. All other transitions","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:9968"}},{"Add":{"text":"with a non-zero probability are walkable in theory and will be unfolded by the","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10047"}},{"Add":{"text":"partial evaluation. Hence they must be considered for the set of abstracted","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10123"}},{"Add":{"text":"locations in order to guarantee termination of the algorithm.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10185"}},{"Add":{"text":"If a path has should result in a zero-probability, this could be filtered during","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10266"}},{"Add":{"text":"partial evaluation. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10287"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10288"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":82,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":311}],"down_context":[{"change":3,"pos":269}],"flag":"BLOCK","start":10290,"end":10360,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\Rs}[0]{\\mathfrak{R}} % the structure of real arithmetic.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10359"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":91,"ins":{"up_context":[{"change":3,"pos":375}],"down_context":[{"change":3,"pos":343}],"flag":"BLOCK","start":10361,"end":10433,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":375},"to":{"change":3,"start":375,"end":435},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\newcommand{\\set}[2]{\\left\\{ #1\\hspace{0.5em}|\\hspace{0.5em}#2\\right\\}}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10432"}}],"del_contents":[{"Del":{"text":"\\newcommand{\\set}[2]{\\{#1\\hspace{0.5em}|\\hspace{0.5em}#2\\}}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:434"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":94,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":445}],"down_context":[{"change":3,"pos":162}],"flag":"BLOCK","start":10434,"end":10639,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\section{Preliminaries}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10457"}},{"Add":{"text":"Let $\\Zs := (\\Z, +, \\cdot, 0, 1, \\leq, <, =)$ be the structure standard integer","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10537"}},{"Add":{"text":"arithmetic, and $\\Rs := (\\R, +, \\cdot, 0, 1, \\leq, <, =)$ the structure of","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10612"}},{"Add":{"text":"standard real arithmetic.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10638"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":100,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":20544}],"down_context":[{"change":3,"pos":777}],"flag":"BLOCK","start":10640,"end":10735,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"In the following $\\V$ denotes a countable finite set of variables $\\V = \\{v_1,","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10718"}},{"Add":{"text":"\\dots, v_n\\}$. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10734"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":103,"ins":{"up_context":[{"change":3,"pos":778}],"down_context":[{"change":3,"pos":1406}],"flag":"BLOCK","start":10736,"end":11231,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":778},"to":{"change":3,"start":778,"end":852},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":852},"to":{"change":3,"start":2989,"end":3069},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":3069},"to":{"change":3,"start":865,"end":866},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":865},"to":{"change":3,"start":865,"end":866},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":866},"to":{"change":3,"start":1034,"end":1065},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1034},"to":{"change":3,"start":1034,"end":1065},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1065},"to":{"change":3,"start":3070,"end":3379},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{definition}[Constraints]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10767"}},{"Add":{"text":" For a given finite set of variables $\\V$, the set of \\textit{linear","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10839"}},{"Add":{"text":" non-strict inequality constraints} is defined as the set $\\L^{\\leq}$:","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10913"}},{"Add":{"text":" \\begin{align}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10931"}},{"Add":{"text":" \\L^{\\leq}=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i \\leq 0}{a_i \\in \\R}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11003"}},{"Add":{"text":" \\end{align}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11019"}},{"Add":{"text":" Analogously, the set of \\textit{linear strict inequality} constraints is","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11096"}},{"Add":{"text":" defined as the set $\\L^{<}$:","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11129"}},{"Add":{"text":" \\begin{align}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11147"}},{"Add":{"text":" \\L^{<}:=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i < 0}{a_i \\in \\R}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11214"}},{"Add":{"text":" \\end{align}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11230"}}],"del_contents":[{"Del":{"text":"Let $\\Zs := (\\Z, +, \\cdot, 0, 1, <)$ be the structure of ordered standard","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:851"}},{"Del":{"text":"integer arithmetic. Let $\\V = \\{v_1, \\dots v_n\\}$ be a finite set of variables.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3068"}},{"Del":{"text":"","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:865"}},{"Del":{"text":"\\begin{definition}[Constraint]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1064"}},{"Del":{"text":" For a given finite set of variables $\\V$, the set of \\textit{linear}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3142"}},{"Del":{"text":" constraints $\\L$ over the variables $\\V$ is defined as the set $\\set{a_0 +","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3221"}},{"Del":{"text":" \\sum_{i=1}^{|\\V|} a_i v_i < 0}{a_i \\in \\Z}$. The set of","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3281"}},{"Del":{"text":" \\textit{polynomial} constraints $\\C$ is defined as the set $\\set{e < 0}{e","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3359"}},{"Del":{"text":" \\in \\Z[\\V]}$. ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3378"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":116,"ins":{"up_context":[{"change":3,"pos":3381}],"down_context":[{"change":3,"pos":956}],"flag":"BLOCK","start":11232,"end":11347,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":3,"pos":3381},"to":{"change":3,"start":867,"end":942},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1441},"to":{"change":3,"start":867,"end":942},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":942},"to":{"change":3,"start":3382,"end":3395},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"The union of strict and non-strict linear constraints is called \\textit{mixed}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11310"}},{"Add":{"text":"linear constraints denoted as $\\L$.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11346"}}],"del_contents":[{"Del":{"text":"Constraints are a subset of FO-formulas and thus the semantics are defined","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:941"}},{"Del":{"text":"accordingly.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3394"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":119,"ins":{"up_context":[{"change":3,"pos":957}],"down_context":[{"change":3,"pos":482}],"flag":"BLOCK","start":11348,"end":11443,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":3,"pos":957},"to":{"change":3,"start":1548,"end":1583},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1548},"to":{"change":3,"start":1548,"end":1583},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1583},"to":{"change":3,"start":958,"end":1108},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1108},"to":{"change":3,"start":1742,"end":1843},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1742},"to":{"change":3,"start":1742,"end":1843},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"Constraints are a subset of FO-formulas and thus their semantics shall be","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11421"}},{"Add":{"text":"defined accordingly.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11442"}}],"del_contents":[{"Del":{"text":"\\begin{definition}[Satisfiability]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1582"}},{"Del":{"text":" A constraint $c \\in \\C$ is \\textit{satisfiable} when the formula $c$ is","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1033"}},{"Del":{"text":" satisfiable in $\\Zs$ or $\\Zs \\models c$. We say a variable assignment","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1107"}},{"Del":{"text":" $\\beta: \\V \\mapsto \\Z$ \\textit{satisfies} the constraint $c$ when $(\\Zs,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1818"}},{"Del":{"text":" \\beta) \\models c$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1842"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":122,"ins":{"up_context":[{"change":3,"pos":483}],"down_context":[{"change":3,"pos":2203}],"flag":"BLOCK","start":11444,"end":11832,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":483},"to":{"change":3,"start":1844,"end":2159},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2159},"to":{"change":3,"start":3396,"end":3440},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{definition}[Satisfiability]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11478"}},{"Add":{"text":" For a domain $D$ and a structure $\\mathfrak{I} = (D, +, \\cdot, 0, 1, \\leq,","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11557"}},{"Add":{"text":" <, =)$, a constraint $\\psi \\in \\L$ is \\textit{satisfiable} in when the formula","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11640"}},{"Add":{"text":" $\\psi$ is $\\mathfrak{I} \\models \\psi$. We say a variable assignment $\\beta: \\V","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11723"}},{"Add":{"text":" \\rightarrow D$ \\textit{satisfies} the constraint $\\psi$ when $(\\mathfrak{I},","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11804"}},{"Add":{"text":" \\beta) \\models \\psi$. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11831"}}],"del_contents":[{"Del":{"text":" Analogously, satisfiability of a set of constraints is defined by the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1917"}},{"Del":{"text":" satisfiability of its conjunction. A set of constraints $C \\subseteq \\C$ is","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1997"}},{"Del":{"text":" \\textit{satisfiable} when $\\Zs \\models \\LAnd_{c_i \\in C} c_i$. Moreover, an","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2077"}},{"Del":{"text":" assignment $\\beta$ \\textit{satisfies} the set of constraints $C$ when $(\\Zs,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2158"}},{"Del":{"text":" \\beta) \\models \\LAnd_{c_i \\in C} c_i$. ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3439"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":130,"ins":{"up_context":[{"change":3,"pos":1087}],"down_context":[{"change":3,"pos":1249}],"flag":"BLOCK","start":11833,"end":12230,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1087},"to":{"change":3,"start":2221,"end":2295},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2295},"to":{"change":3,"start":1155,"end":1249},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"A set of constraints $C \\subseteq \\L$ is satisfiable, when their conjunction is","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11912"}},{"Add":{"text":"satisfiable and we write $\\mathfrak{I} \\models C$ instead of $\\mathfrak{I}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11987"}},{"Add":{"text":"\\models \\LAnd_{\\psi_i \\in C} \\psi_i$. In addition whenever the structure is evident","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12071"}},{"Add":{"text":"from context, we write $\\models \\psi$ and $\\beta \\models \\psi$ instead of","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12145"}},{"Add":{"text":"$\\mathfrak{I} \\models \\psi$ and $(\\mathfrak{I}, \\beta) \\models \\psi$ respectively. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12229"}}],"del_contents":[{"Del":{"text":"We also write $\\Zs \\models C$ and $(\\Zs, \\beta)\\models C$ instead of $\\Zs","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2294"}},{"Del":{"text":"\\models \\LAnd_{c_i \\in C} c_i$ and $(\\Zs, \\beta)\\models \\LAnd_{c_i \\in C} c_i$,","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1234"}},{"Del":{"text":"respectively.","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1248"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":140,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1460},"to":{"change":3,"start":1460,"end":1618},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1618},"to":{"change":3,"start":3441,"end":3474},"introduced_by":3}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":" Correspondingly, $\\llbracket c \\rrbracket$ and $\\llbracket C \\rrbracket$ are","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1540"}},{"Del":{"text":" the solutions of the constraint $c \\in \\C$ and the set of constraints $C","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1617"}},{"Del":{"text":" \\subseteq \\C$, respectively.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3473"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":142,"ins":{"up_context":[{"change":3,"pos":1667}],"down_context":[{"change":3,"pos":3475}],"flag":"BLOCK","start":12231,"end":12335,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1667},"to":{"change":3,"start":1667,"end":1766},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"The following properties hold. Hence, conjunctions and sets of constraints can","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12309"}},{"Add":{"text":"be used interchangeably.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12334"}}],"del_contents":[{"Del":{"text":"The following properties hold. Hence, we use conjunctions and sets of","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1736"}},{"Del":{"text":"constraints interchangeably.","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1765"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":145,"ins":{"up_context":[{"change":3,"pos":3489}],"down_context":[{"change":3,"pos":3704}],"flag":"BLOCK","start":12336,"end":12607,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":3489},"to":{"change":3,"start":3489,"end":3568},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":3568},"to":{"change":3,"start":1861,"end":1894},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1861},"to":{"change":3,"start":1861,"end":1894},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1894},"to":{"change":3,"start":3569,"end":3704},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" \\llbracket \\psi_1 \\Land \\psi_2 \\rrbracket = \\llbracket \\psi_1 \\rrbracket \\intersect","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12423"}},{"Add":{"text":" \\llbracket \\psi_2 \\rrbracket \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12459"}},{"Add":{"text":" \\llbracket C \\rrbracket = \\llbracket \\LAnd_{\\psi_i \\in C} \\psi_i \\rrbracket ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12540"}},{"Add":{"text":" = \\Intersect_{\\psi_i \\in C} \\llbracket \\psi_i \\rrbracket","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12606"}}],"del_contents":[{"Del":{"text":" \\llbracket c_1 \\Land c_2 \\rrbracket = \\llbracket c_1 \\rrbracket \\intersect","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3567"}},{"Del":{"text":" \\llbracket c_2 \\rrbracket \\\\","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:1893"}},{"Del":{"text":" \\llbracket C \\rrbracket = \\llbracket \\LAnd_{c_i \\in C} c_i \\rrbracket ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3643"}},{"Del":{"text":" = \\Intersect_{c_i \\in C} \\llbracket c_i \\rrbracket","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3703"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":152,"ins":{"up_context":[{"change":3,"pos":2079}],"down_context":[{"change":3,"pos":2234}],"flag":"BLOCK","start":12608,"end":12777,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2079},"to":{"change":3,"start":2079,"end":2234},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" Two formulas, constraints, or set of constraints are considered","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12675"}},{"Add":{"text":" \\textit{equivalent}, denoted as $\\varphi_1 \\equiv \\varphi_2$ when there","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12751"}},{"Add":{"text":" solutions are equal.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12776"}}],"del_contents":[{"Del":{"text":" Two formulas, constraints, or set of constraints are considered equivalent,","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:2158"}},{"Del":{"text":" when there solutions are equal. We write $\\varphi_1 \\equiv \\varphi_2$.","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:2233"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":156,"atom":{"EdgeMap":{"edges":[{"previous":"","flag":"DELETED","from":{"change":3,"pos":2251},"to":{"change":3,"start":2464,"end":2545},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2464},"to":{"change":3,"start":2464,"end":2545},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2545},"to":{"change":3,"start":3717,"end":3798},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":3798},"to":{"change":3,"start":2621,"end":2700},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2621},"to":{"change":3,"start":2621,"end":2700},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2700},"to":{"change":3,"start":2252,"end":2332},"introduced_by":3}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":"","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2464"}},{"Del":{"text":"Note that by definition constraints are restricted to the form $e < 0$, because","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2544"}},{"Del":{"text":"\\gls{koat} uses this representation internally and it makes proofs more concise.","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3797"}},{"Del":{"text":"However, all constraint $e_1 \\diamond e_2$ with the operators $\\diamond \\in >,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2699"}},{"Del":{"text":"<, \\leq, \\geq$ can be transformed into equivalent constraints $e' < 0 \\in \\C$: ","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:2331"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":157,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":2781}],"down_context":[{"change":3,"pos":1087}],"flag":"BLOCK","start":12778,"end":13115,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"In practice constraints are often provided in a more general form. Restricting","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12856"}},{"Add":{"text":"the constraints to a specific form does not limit it's practicality, since they","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:12936"}},{"Add":{"text":"can be easily converted into one of those forms. Constraints of the form $e_1","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13014"}},{"Add":{"text":"\\diamond e_2$ with the operators $\\diamond \\in \\{=, >, <, \\leq, \\geq\\}$ can","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13090"}},{"Add":{"text":"transformed as follows:","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13114"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":163,"ins":{"up_context":[{"change":3,"pos":1102}],"down_context":[{"change":3,"pos":2827}],"flag":"BLOCK","start":13116,"end":13206,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1102},"to":{"change":3,"start":1102,"end":1148},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1148},"to":{"change":3,"start":2782,"end":2827},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" e_1 \\leq e_2 &\\equiv e_1 - e_2 \\leq 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13160"}},{"Add":{"text":" e_1 \\geq e_2 &\\equiv e_2 - e_1 \\leq 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13205"}}],"del_contents":[{"Del":{"text":" e_1 \\geq e_2 &\\equiv e_2 - e_1 - 1 < 0 \\\\","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1147"}},{"Del":{"text":" e_1 \\leq e_2 &\\equiv e_1 - e_2 - 1< 0 \\\\","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2826"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":166,"ins":{"up_context":[{"change":3,"pos":2866}],"down_context":[{"change":3,"pos":1187}],"flag":"BLOCK","start":13207,"end":13365,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2866},"to":{"change":3,"start":2866,"end":2902},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" e_1 < e_2 &\\equiv e_1 - e_2 < 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13245"}},{"Add":{"text":" e_1 = e_2 &\\equiv e_1 \\leq e_2 \\land e_2 \\leq e_1 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13302"}},{"Add":{"text":" &\\equiv e_1 - e_2 \\leq 0 \\land e_2 - e_1 \\leq 0","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13364"}}],"del_contents":[{"Del":{"text":" e_1 < e_2 &\\equiv e_1 - e_2 < 0","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2901"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":171,"ins":{"up_context":[{"change":3,"pos":1435}],"down_context":[{"change":3,"pos":1691}],"flag":"BLOCK","start":13366,"end":13784,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1435},"to":{"change":3,"start":2903,"end":2950},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"For real arithmetic it is important to distinguish between strict and non-strict","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13446"}},{"Add":{"text":"constraints, however for integer arithmetic it is enough to consider only strict","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13527"}},{"Add":{"text":"inequality as one can be transformed into the other: ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13581"}},{"Add":{"text":"\\begin{align*}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13596"}},{"Add":{"text":" e_1 \\geq e_2 &\\equiv e_2 - e_1 - 1 < 0 \\\\","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13642"}},{"Add":{"text":" e_1 \\leq e_2 &\\equiv e_1 - e_2 - 1< 0","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13684"}},{"Add":{"text":"\\end{align*}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13697"}},{"Add":{"text":"When talking about integer arithmetic we will thus only refer to linear","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13769"}},{"Add":{"text":"constraints. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13783"}}],"del_contents":[{"Del":{"text":"Equality can be simulated by two constraints. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2949"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":181,"ins":{"up_context":[{"change":3,"pos":1692}],"down_context":[{"change":3,"pos":1801}],"flag":"BLOCK","start":13785,"end":13840,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1692},"to":{"change":3,"start":2951,"end":3038},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\section{Abstract Domains}\\label{sec:abstract_domains}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13839"}}],"del_contents":[{"Del":{"text":"\\begin{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2968"}},{"Del":{"text":" e_1 = e_2 \\equiv e_1 \\leq e_2 \\Land e_1 \\geq e_2","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3021"}},{"Del":{"text":"\\end{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3037"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":183,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1802},"to":{"change":3,"start":3799,"end":3954},"introduced_by":3}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":"Hence, we will use the all operators above, whenever it improves readability,","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3876"}},{"Del":{"text":"but assume the constraints to be of the simplified form, in formal proofs. ","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3952"}},{"Del":{"text":"","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:3953"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":312,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":9406}],"down_context":[{"change":3,"pos":9406}],"flag":"BLOCK","start":13841,"end":14075,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\subsection{Abstract domains}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13870"}},{"Add":{"text":"An abstract domain is a representation for a set of points in an eu","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13938"}},{"Add":{"text":"Polyhedron\\cite{bagnara2005convexpolyhedron}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:13983"}},{"Add":{"text":"Octagons\\cite{mine2001wcre, mine2007arxiv, mine2006hosc,truchet2010synacs}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14058"}},{"Add":{"text":"Interval domain","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14074"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":318,"ins":{"up_context":[{"change":3,"pos":9407}],"down_context":[{"change":3,"pos":2525}],"flag":"BLOCK","start":14076,"end":15122,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":9407},"to":{"change":2,"start":21213,"end":21268},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"Among others the following operations are important to our use-case.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14144"}},{"Add":{"text":"1. Emptiness","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14157"}},{"Add":{"text":"2. Intersection","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14173"}},{"Add":{"text":"3. Inclusion test","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14191"}},{"Add":{"text":"3. Orthogonal projection","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14216"}},{"Add":{"text":"4. Upper and lower bounds","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14242"}},{"Add":{"text":"\\subsection{Not necessarily closed convex polyhedra}\\label{ssec:nncpolyhedra}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14320"}},{"Add":{"text":"Taking the definitions from \\cite{bagnara2005convexpolyhedron} a set of linear","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14399"}},{"Add":{"text":"constraints exactly defines a polyhedron. Every linear non-strict inequality","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14476"}},{"Add":{"text":"constraint $\\psi \\in \\L^{\\leq}$ describes an closed affine half-space and every","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14556"}},{"Add":{"text":"linear strict inequality constraint $\\psi \\in \\L^{\\leq}$ describes an open","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14631"}},{"Add":{"text":"affine half-space in the euclidean space $\\R^n$. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14681"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14682"}},{"Add":{"text":"\\begin{definition}[Not necessarily closed Polyhedra]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14735"}},{"Add":{"text":" $\\mathcal{P} \\subseteq \\R^n$ is a closed (convex) polyhedron if and only if","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14815"}},{"Add":{"text":" it can be expressed by an intersection of a finite number of not necessarily","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14896"}},{"Add":{"text":" closed affine half-spaces.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14927"}},{"Add":{"text":"\\end{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14944"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14945"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14946"}},{"Add":{"text":"\\subsection{Octagons}\\label{ssec:octagons}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14989"}},{"Add":{"text":"The octagon domain was constructed to bridge the performance gap between","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15062"}},{"Add":{"text":"intervals (see \\Sref{ssec:intervals below} and polyhedra. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15121"}}],"del_contents":[{"Del":{"text":"% \\subsection{Convex Polyhedron}\\label{sec:polyhedron}","pos":"RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC:21267"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":342,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":2526}],"down_context":[{"change":2,"pos":21269}],"flag":"BLOCK","start":15123,"end":16422,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"An octagon can be described by a set of constraints of the form $\\pm v_i \\pm v_j","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15203"}},{"Add":{"text":"\\leq b$\\cite{mine2001wcre}. Obviously, such constraints are linear constraints","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15282"}},{"Add":{"text":"and hence octagons are a specialization of polyhedra. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15337"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15338"}},{"Add":{"text":"Octagons are used in \\gls{koat} during the computation of invariants. They are","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15417"}},{"Add":{"text":"faster to work with than polyhedra but less precise. \\todo{cite runtime for","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15493"}},{"Add":{"text":"various operations} As shown in \\Sref{sec:invariant}, too wide constraints are","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15572"}},{"Add":{"text":"not a problem for invariants. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15603"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15604"}},{"Add":{"text":"\\subsection{Intervals}\\label{ssec:intervals}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15649"}},{"Add":{"text":"For completes sake, let's introduce a third abstract domain: the interval","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15723"}},{"Add":{"text":"domain. An closed interval $[a,b]$ with $a, b \\in \\R$ for a variable $v \\in \\V$","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15803"}},{"Add":{"text":"can be expressed as a pair of linear constraints of the form $a \\leq v$ and $v","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15882"}},{"Add":{"text":"\\leq b$.","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15891"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15892"}},{"Add":{"text":"\\begin{definition}[Box]","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15916"}},{"Add":{"text":" $mathcal{B} \\subseteq \\R^n$ is a box if it can be expressed by a set of","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:15992"}},{"Add":{"text":" intervals. ","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16008"}},{"Add":{"text":"\\end{definition}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16025"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16026"}},{"Add":{"text":"By construction every Box is an octagon and in turn a polyhedron. For every","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16102"}},{"Add":{"text":"polyhedron $P$ one can find a box $B$ that includes the polyhedron. Whenever","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16179"}},{"Add":{"text":"it's acceptable to arbitrarily widen the polyhedron, one can work with boxes","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16256"}},{"Add":{"text":"instead. Boxes are computationally very efficient, although rather imprecise,","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16334"}},{"Add":{"text":"for most applications.\\todo{beautify}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16372"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16373"}},{"Add":{"text":"\\todo{example picture}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16396"}},{"Add":{"text":"","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16397"}},{"Add":{"text":"\\subsection{Operations}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16421"}}]}},{"Edit":{"inode":{"change":13,"pos":11899},"path":"acronyms.tex","line":14,"atom":{"NewVertex":{"up_context":[{"change":13,"pos":12607}],"down_context":[],"flag":"BLOCK","start":16423,"end":16591,"inode":{"change":13,"pos":11899}}},"contents":[{"Add":{"text":"\\newacronym{dfs}{DFS}{depth-first search}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16464"}},{"Add":{"text":"\\newacronym{bfs}{BFS}{breadth-first search}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16508"}},{"Add":{"text":"\\newacronym{lip}{LIP}{linear integer program}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16554"}},{"Add":{"text":"\\newacronym{lp}{LP}{linear program}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:16590"}}]}}],"owner":"paradyx","repo":"ma-tex","token":"H/jqZ9p2EVg0BBjZWk6V0KC39MgvZ8QwpeCAXrWZFzY=","login":null}

…

Dependencies

Change contents

Review