diff options
-rw-r--r-- | abstract/abs_interp_edd.ml | 151 | ||||
-rw-r--r-- | frontend/ast_printer.ml | 25 | ||||
-rw-r--r-- | frontend/parser.mly | 61 | ||||
-rw-r--r-- | tests/Makefile | 3 | ||||
-rw-r--r-- | tests/result/DiffSystem.out | 2002 | ||||
-rw-r--r-- | tests/source/DiffSystem.scade | 34 | ||||
-rw-r--r-- | tests/source/NestedControl.scade | 47 | ||||
-rw-r--r-- | tests/source/Overflows.scade | 43 |
8 files changed, 2240 insertions, 126 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index fd31670..6220a0a 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -280,78 +280,86 @@ end = struct edd_meet : edd_v -> edd_v -> edd_v *) let edd_join a b = - let ve = a.ve in - let leaves, get_leaf = get_leaf_fun () in - let dq = new_node_fun () in - - let f f_rec na nb = - match na, nb with - | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> - let kl = List.map2 - (fun (ta, ba) (tb, bb) -> assert (ta = tb); - ta, f_rec ba bb) - la lb - in - dq va kl - - | DTop, _ | _, DTop -> DTop - | DBot, DBot -> DBot - - | DChoice(_,va, la), _ when rank ve na < rank ve nb -> - let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in - dq va kl - | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> - let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in - dq vb kl - - | DVal (u, _), DVal (v, _) -> - let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x - | DVal(u, _), DBot -> - get_leaf (Hashtbl.find a.leaves u) - | DBot, DVal(v, _) -> - get_leaf (Hashtbl.find b.leaves v) - - | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *) - in - { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } + if a.root = DBot then b else + if b.root = DBot then a else + if a.root = DTop || b.root = DTop then edd_top a.ve else begin + let ve = a.ve in + let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in + + let f f_rec na nb = + match na, nb with + | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f_rec ba bb) + la lb + in + dq va kl + + | DTop, _ | _, DTop -> DTop + | DBot, DBot -> DBot + + | DChoice(_,va, la), _ when rank ve na < rank ve nb -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + + | DVal (u, _), DVal (v, _) -> + let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + | DVal(u, _), DBot -> + get_leaf (Hashtbl.find a.leaves u) + | DBot, DVal(v, _) -> + get_leaf (Hashtbl.find b.leaves v) + + | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *) + in + { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) } + end let edd_meet a b = - let ve = a.ve in - let leaves, get_leaf = get_leaf_fun () in - let dq = new_node_fun () in - - let f f_rec na nb = - match na, nb with - | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> - let kl = List.map2 - (fun (ta, ba) (tb, bb) -> assert (ta = tb); - ta, f_rec ba bb) - la lb - in - dq va kl - - | DBot, _ | _, DBot -> DBot - | DTop, DTop -> DTop - - | DChoice(_, va, la), _ when rank ve na < rank ve nb -> - let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in - dq va kl - | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> - let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in - dq vb kl - - | DVal (u, _) , DVal (v, _) -> - let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in - get_leaf x - | DVal(u, _), DTop -> - get_leaf (Hashtbl.find a.leaves u) - | DTop, DVal(v, _) -> - get_leaf (Hashtbl.find b.leaves v) - - | _ -> assert false (* see above *) - in - { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } + if a.root = DTop then b else + if b.root = DTop then a else + if a.root = DBot || b.root = DBot then edd_bot a.ve else begin + let ve = a.ve in + let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in + + let f f_rec na nb = + match na, nb with + | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f_rec ba bb) + la lb + in + dq va kl + + | DBot, _ | _, DBot -> DBot + | DTop, DTop -> DTop + + | DChoice(_, va, la), _ when rank ve na < rank ve nb -> + let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in + dq va kl + | _, DChoice(_, vb, lb) when rank ve nb < rank ve na -> + let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in + dq vb kl + + | DVal (u, _) , DVal (v, _) -> + let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + | DVal(u, _), DTop -> + get_leaf (Hashtbl.find a.leaves u) + | DTop, DVal(v, _) -> + get_leaf (Hashtbl.find b.leaves v) + + | _ -> assert false (* see above *) + in + { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) } + end @@ -407,7 +415,8 @@ end = struct | CLFalse -> edd_bot v.ve | CLAnd (a, b) -> let v = edd_apply_cl v ([], nc, a) in - edd_apply_cl v ([], nc, b) + if v.root = DBot then v else + edd_apply_cl v ([], nc, b) | CLOr((eca, nca, ra), (ecb, ncb, rb)) -> edd_join (edd_apply_cl v (eca, nc@nca, ra)) (edd_apply_cl v (ecb, nc@ncb, rb)) diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 3ca2ff6..8908687 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -165,12 +165,15 @@ let rec print_expr fmt e = let indent ind = ind^" " -let rec print_vars ind fmt = function - | [] -> () - | v -> +let rec print_scope ind fmt = function + | [], [a, _] -> + print_eqn ind fmt a + | [], l -> print_body ind fmt l + | v, l -> Format.fprintf fmt "%svar" ind; List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) v; Format.fprintf fmt "@\n"; + print_body ind fmt l and print_var_decl fmt (pr, i, ty) = Format.fprintf fmt "%s%s: %s" @@ -182,6 +185,9 @@ and print_body ind fmt body = Format.fprintf fmt "%slet@\n%a%stel@\n" ind (print_block ind) body ind +and print_block ind fmt b = + List.iter (fun (bb,_) -> print_eqn (indent ind) fmt bb) b + and print_eqn ind fmt = function | AST_assign (l,(e,_)) -> Format.fprintf fmt "%s%a = %a;@\n" @@ -207,8 +213,7 @@ and print_activate_if ind fmt = function Format.fprintf fmt "%selse@\n" ind; print_activate_if (indent ind) fmt e | AST_activate_body(b) -> - print_vars ind fmt b.act_locals; - print_body ind fmt b.body + print_scope ind fmt (b.act_locals, b.body) and print_automaton ind fmt (n, sts, r) = Format.fprintf fmt "%sautomaton %s@\n" ind n; @@ -218,8 +223,8 @@ and print_automaton ind fmt (n, sts, r) = and print_state ind fmt (st, _) = Format.fprintf fmt "%s%sstate %s@\n" ind (if st.initial then "initial " else "") st.st_name; - print_vars ind fmt st.st_locals; - print_body ind fmt st.body; + let ind = indent ind in + print_scope ind fmt (st.st_locals, st.body); if st.until <> [] then begin Format.fprintf fmt "%suntil@\n" ind; List.iter (fun ((e, _),(s, _), reset) -> @@ -227,9 +232,6 @@ and print_state ind fmt (st, _) = st.until end -and print_block ind fmt b = - List.iter (fun (bb,_) -> print_eqn (indent ind) fmt bb) b - (* declarations *) @@ -238,8 +240,7 @@ and print_node_decl fmt (d : node_decl) = d.n_name (print_list print_var_decl "; ") d.args (print_list print_var_decl "; ") d.ret; - print_vars "" fmt d.var; - print_body "" fmt d.body + print_scope "" fmt (d.var, d.body) let print_const_decl fmt (d : const_decl) = Format.fprintf fmt diff --git a/frontend/parser.mly b/frontend/parser.mly index 84dcd15..e8a6ecf 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -117,27 +117,16 @@ automaton: state: | i=boption(INITIAL) STATE n=IDENT unless=trans(UNLESS) - v=option(var_decl) - b=body + vb=scbody until=trans(UNTIL) { if unless <> [] then failwith "UNLESS transitions not supported."; + let v, b = vb in { initial = i; st_name = n; - st_locals = (match v with Some v -> v | None -> []); + st_locals = v; body = b; until = until; } } -| i=boption(INITIAL) STATE n=IDENT - unless=trans(UNLESS) - b=ext(eqn) SEMICOLON - until=trans(UNTIL) -{ if unless <> [] then failwith "UNLESS transitions not supported."; - { initial = i; - st_name = n; - st_locals = []; - body = [b]; - until = until; -} } trans(TT): | TT t=nonempty_list(terminated(transition, SEMICOLON)) { t } @@ -151,11 +140,12 @@ activate: | ACTIVATE a=activate_if RETURNS r=separated_list(COMMA, IDENT) { (a, r) } activate_if: | IF c=ext(expr) THEN t=activate_if ELSE e=activate_if { AST_activate_if(c, t, e) } -| lv=option(var_decl) b=body -{ AST_activate_body { +| kb=scbody +{ let loc, body = kb in + AST_activate_body { act_id = "act"^uid(); - act_locals = (match lv with Some v -> v | None -> []); - body = b; + act_locals = loc; + body = body; } } eqn: @@ -172,13 +162,13 @@ typ: | REAL { AST_TREAL } (* Declarations *) -dbody: -| e=ext(eqn) SEMICOLON { [e] } -| l=body { l } - -body: +scbody: +| e=ext(eqn) SEMICOLON { [], [e] } | LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL - { l } + { [], l} +| VAR v=nonempty_list(terminated(vari, SEMICOLON)) + LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL + { List.flatten v, l } var: | p=boption(PROBE) i=IDENT { (p, i) } @@ -199,32 +189,19 @@ const_decl: value = e; } } -var_decl: -| VAR l=nonempty_list(terminated(vari, SEMICOLON)) - { List.flatten l } - node_kw: | NODE {} | FUNCTION {} node_decl: | node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN - e = dbody -{ { n_name = id; - args = v; - ret = rv; - var = []; - body = e; -} } -| node_kw id=IDENT LPAREN v=vars RPAREN - RETURNS LPAREN rv=vars RPAREN - lv=var_decl - b=body -{ { n_name = id; + sc=scbody +{ let vars, body = sc in + { n_name = id; args = v; ret = rv; - var = lv; - body = b; + var = vars; + body = body; } } (* Utility : add extent information *) diff --git a/tests/Makefile b/tests/Makefile index 24df589..3631d67 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -5,7 +5,8 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.out \ result/test6.out result/testc.out \ result/gilbreath.out result/half.out result/updown2.out \ result/abro.out \ - result/rfollow.out result/cosinus.out + result/rfollow.out result/cosinus.out \ + result/DiffSystem.out bin/%.test: source/%.scade test.c rm kcg/* diff --git a/tests/result/DiffSystem.out b/tests/result/DiffSystem.out new file mode 100644 index 0000000..ec10f60 --- /dev/null +++ b/tests/result/DiffSystem.out @@ -0,0 +1,2002 @@ +0. 1000 0 1 +1. 1000 0 3 +2. 1000 0 5 +3. 1000 0 6 +4. 1000 0 8 +5. 1000 0 10 +6. 1000 0 12 +7. 1000 0 13 +8. 1000 0 15 +9. 1000 0 17 +10. 1000 0 18 +11. 1000 0 20 +12. 1000 0 22 +13. 1000 0 24 +14. 1000 0 25 +15. 1000 0 27 +16. 1000 0 29 +17. 1000 0 30 +18. 1000 0 32 +19. 1000 0 34 +20. 1000 0 36 +21. 1000 0 37 +22. 1000 0 39 +23. 1000 0 41 +24. 1000 0 42 +25. 1000 0 44 +26. 1000 0 46 +27. 1000 0 47 +28. 1000 0 49 +29. 1000 0 51 +30. 1000 0 52 +31. 1000 0 54 +32. 1000 0 56 +33. 1000 0 58 +34. 1000 0 59 +35. 1000 0 61 +36. 1000 0 63 +37. 1000 0 64 +38. 1000 0 66 +39. 1000 0 68 +40. 1000 0 69 +41. 1000 0 71 +42. 1000 0 73 +43. 1000 0 74 +44. 1000 0 76 +45. 1000 0 78 +46. 1000 0 79 +47. 1000 0 81 +48. 1000 0 83 +49. 1000 0 84 +50. 1000 0 86 +51. 1000 0 87 +52. 1000 0 89 +53. 1000 0 91 +54. 1000 0 92 +55. 1000 0 94 +56. 1000 0 96 +57. 1000 0 97 +58. 1000 0 99 +59. 1000 0 101 +60. 1000 0 102 +61. 1000 0 104 +62. 1000 0 105 +63. 1000 0 107 +64. 1000 0 109 +65. 1000 0 110 +66. 1000 0 112 +67. 1000 0 114 +68. 1000 0 115 +69. 1000 0 117 +70. 1000 0 118 +71. 1000 0 120 +72. 1000 0 122 +73. 1000 0 123 +74. 1000 0 125 +75. 1000 0 126 +76. 1000 0 128 +77. 1000 0 130 +78. 1000 0 131 +79. 1000 0 133 +80. 1000 0 134 +81. 1000 0 136 +82. 1000 0 137 +83. 1000 0 139 +84. 1000 0 141 +85. 1000 0 142 +86. 1000 0 144 +87. 1000 0 145 +88. 1000 0 147 +89. 1000 0 148 +90. 1000 0 150 +91. 1000 0 151 +92. 1000 0 153 +93. 1000 0 154 +94. 1000 0 156 +95. 1000 0 158 +96. 1000 0 159 +97. 1000 0 161 +98. 1000 0 162 +99. 1000 0 164 +100. 1000 0 165 +101. 1000 0 167 +102. 1000 0 168 +103. 1000 0 170 +104. 1000 0 171 +105. 1000 0 173 +106. 1000 0 174 +107. 1000 0 176 +108. 1000 0 177 +109. 1000 0 179 +110. 1000 0 180 +111. 1000 0 182 +112. 1000 0 183 +113. 1000 0 185 +114. 1000 0 186 +115. 1000 0 187 +116. 1000 0 189 +117. 1000 0 190 +118. 1000 0 192 +119. 1000 0 193 +120. 1000 0 195 +121. 1000 0 196 +122. 1000 0 198 +123. 1000 0 199 +124. 1000 0 200 +125. 1000 0 202 +126. 1000 0 203 +127. 1000 0 205 +128. 1000 0 206 +129. 1000 0 208 +130. 1000 0 209 +131. 1000 0 210 +132. 1000 0 212 +133. 1000 0 213 +134. 1000 0 215 +135. 1000 0 216 +136. 1000 0 217 +137. 1000 0 219 +138. 1000 0 220 +139. 1000 0 221 +140. 1000 0 223 +141. 1000 0 224 +142. 1000 0 226 +143. 1000 0 227 +144. 1000 0 228 +145. 1000 0 230 +146. 1000 0 231 +147. 1000 0 232 +148. 1000 0 234 +149. 1000 0 235 +150. 1000 0 236 +151. 1000 0 238 +152. 1000 0 239 +153. 1000 0 240 +154. 1000 0 242 +155. 1000 0 243 +156. 1000 0 244 +157. 1000 0 246 +158. 1000 0 247 +159. 1000 0 248 +160. 1000 0 250 +161. 1000 0 251 +162. 1000 0 252 +163. 1000 0 253 +164. 1000 0 255 +165. 1000 0 256 +166. 1000 0 257 +167. 1000 0 259 +168. 1000 0 260 +169. 1000 0 261 +170. 1000 0 262 +171. 1000 0 264 +172. 1000 0 265 +173. 1000 0 266 +174. 1000 0 267 +175. 1000 0 269 +176. 1000 0 270 +177. 1000 0 271 +178. 1000 0 272 +179. 1000 0 273 +180. 1000 0 275 +181. 1000 0 276 +182. 1000 0 277 +183. 1000 0 278 +184. 1000 0 279 +185. 1000 0 281 +186. 1000 0 282 +187. 1000 0 283 +188. 1000 0 284 +189. 1000 0 285 +190. 1000 0 287 +191. 1000 0 288 +192. 1000 0 289 +193. 1000 0 290 +194. 1000 0 291 +195. 1000 0 292 +196. 1000 0 294 +197. 1000 0 295 +198. 1000 0 296 +199. 1000 0 297 +200. 1000 0 298 +201. 1000 0 299 +202. 1000 0 300 +203. 1000 0 302 +204. 1000 0 303 +205. 1000 0 304 +206. 1000 0 305 +207. 1000 0 306 +208. 1000 0 307 +209. 1000 0 308 +210. 1000 0 309 +211. 1000 0 310 +212. 1000 0 312 +213. 1000 0 313 +214. 1000 0 314 +215. 1000 0 315 +216. 1000 0 316 +217. 1000 0 317 +218. 1000 0 318 +219. 1000 0 319 +220. 1000 0 320 +221. 1000 0 321 +222. 1000 0 322 +223. 1000 0 323 +224. 1000 0 324 +225. 1000 0 325 +226. 1000 0 326 +227. 1000 0 327 +228. 1000 0 328 +229. 1000 0 329 +230. 1000 0 330 +231. 1000 0 331 +232. 1000 0 332 +233. 1000 0 333 +234. 1000 0 334 +235. 1000 0 335 +236. 1000 0 336 +237. 1000 0 337 +238. 1000 0 338 +239. 1000 0 339 +240. 1000 0 340 +241. 1000 0 341 +242. 1000 0 342 +243. 1000 0 343 +244. 1000 0 344 +245. 1000 0 345 +246. 1000 0 346 +247. 1000 0 347 +248. 1000 0 348 +249. 1000 0 349 +250. 1000 0 350 +251. 1000 0 351 +252. 1000 0 352 +253. 1000 0 353 +254. 1000 0 354 +255. 1000 0 355 +256. 1000 0 356 +257. 1000 0 357 +258. 1000 0 357 +259. 1000 0 358 +260. 1000 0 359 +261. 1000 0 360 +262. 1000 0 361 +263. 1000 0 362 +264. 1000 0 363 +265. 1000 0 364 +266. 1000 0 365 +267. 1000 0 365 +268. 1000 0 366 +269. 1000 0 367 +270. 1000 0 368 +271. 1000 0 369 +272. 1000 0 370 +273. 1000 0 371 +274. 1000 0 371 +275. 1000 0 372 +276. 1000 0 373 +277. 1000 0 374 +278. 1000 0 375 +279. 1000 0 376 +280. 1000 0 377 +281. 1000 0 377 +282. 1000 0 378 +283. 1000 0 379 +284. 1000 0 380 +285. 1000 0 381 +286. 1000 0 381 +287. 1000 0 382 +288. 1000 0 383 +289. 1000 0 384 +290. 1000 0 385 +291. 1000 0 385 +292. 1000 0 386 +293. 1000 0 387 +294. 1000 0 388 +295. 1000 0 389 +296. 1000 0 389 +297. 1000 0 390 +298. 1000 0 391 +299. 1000 0 392 +300. 1000 0 392 +301. 1000 0 393 +302. 1000 0 394 +303. 1000 0 395 +304. 1000 0 395 +305. 1000 0 396 +306. 1000 0 397 +307. 1000 0 398 +308. 1000 0 398 +309. 1000 0 399 +310. 1000 0 400 +311. 1000 0 401 +312. 1000 0 401 +313. 1000 0 402 +314. 1000 0 403 +315. 1000 0 403 +316. 1000 0 404 +317. 1000 0 405 +318. 1000 0 405 +319. 1000 0 406 +320. 1000 0 407 +321. 1000 0 408 +322. 1000 0 408 +323. 1000 0 409 +324. 1000 0 410 +325. 1000 0 410 +326. 1000 0 411 +327. 1000 0 412 +328. 1000 0 412 +329. 1000 0 413 +330. 1000 0 414 +331. 1000 0 414 +332. 1000 0 415 +333. 1000 0 416 +334. 1000 0 416 +335. 1000 0 417 +336. 1000 0 418 +337. 1000 0 418 +338. 1000 0 419 +339. 1000 0 419 +340. 1000 0 420 +341. 1000 0 421 +342. 1000 0 421 +343. 1000 0 422 +344. 1000 0 423 +345. 1000 0 423 +346. 1000 0 424 +347. 1000 0 424 +348. 1000 0 425 +349. 1000 0 426 +350. 1000 0 426 +351. 1000 0 427 +352. 1000 0 427 +353. 1000 0 428 +354. 1000 0 429 +355. 1000 0 429 +356. 1000 0 430 +357. 1000 0 430 +358. 1000 0 431 +359. 1000 0 432 +360. 1000 0 432 +361. 1000 0 433 +362. 1000 0 433 +363. 1000 0 434 +364. 1000 0 434 +365. 1000 0 435 +366. 1000 0 435 +367. 1000 0 436 +368. 1000 0 437 +369. 1000 0 437 +370. 1000 0 438 +371. 1000 0 438 +372. 1000 0 439 +373. 1000 0 439 +374. 1000 0 440 +375. 1000 0 440 +376. 1000 0 441 +377. 1000 0 441 +378. 1000 0 442 +379. 1000 0 442 +380. 1000 0 443 +381. 1000 0 443 +382. 1000 0 444 +383. 1000 0 444 +384. 1000 0 445 +385. 1000 0 446 +386. 1000 0 446 +387. 1000 0 447 +388. 1000 0 447 +389. 1000 0 448 +390. 1000 0 448 +391. 1000 0 448 +392. 1000 0 449 +393. 1000 0 449 +394. 1000 0 450 +395. 1000 0 450 +396. 1000 0 451 +397. 1000 0 451 +398. 1000 0 452 +399. 1000 0 452 +400. 1000 0 453 +401. 1000 0 453 +402. 1000 0 454 +403. 1000 0 454 +404. 1000 0 455 +405. 1000 0 455 +406. 1000 0 456 +407. 1000 0 456 +408. 1000 0 456 +409. 1000 0 457 +410. 1000 0 457 +411. 1000 0 458 +412. 1000 0 458 +413. 1000 0 459 +414. 1000 0 459 +415. 1000 0 460 +416. 1000 0 460 +417. 1000 0 460 +418. 1000 0 461 +419. 1000 0 461 +420. 1000 0 462 +421. 1000 0 462 +422. 1000 0 463 +423. 1000 0 463 +424. 1000 0 463 +425. 1000 0 464 +426. 1000 0 464 +427. 1000 0 465 +428. 1000 0 465 +429. 1000 0 465 +430. 1000 0 466 +431. 1000 0 466 +432. 1000 0 467 +433. 1000 0 467 +434. 1000 0 467 +435. 1000 0 468 +436. 1000 0 468 +437. 1000 0 469 +438. 1000 0 469 +439. 1000 0 469 +440. 1000 0 470 +441. 1000 0 470 +442. 1000 0 470 +443. 1000 0 471 +444. 1000 0 471 +445. 1000 0 472 +446. 1000 0 472 +447. 1000 0 472 +448. 1000 0 473 +449. 1000 0 473 +450. 1000 0 473 +451. 1000 0 474 +452. 1000 0 474 +453. 1000 0 474 +454. 1000 0 475 +455. 1000 0 475 +456. 1000 0 475 +457. 1000 0 476 +458. 1000 0 476 +459. 1000 0 477 +460. 1000 0 477 +461. 1000 0 477 +462. 1000 0 478 +463. 1000 0 478 +464. 1000 0 478 +465. 1000 0 479 +466. 1000 0 479 +467. 1000 0 479 +468. 1000 0 480 +469. 1000 0 480 +470. 1000 0 480 +471. 1000 0 480 +472. 1000 0 481 +473. 1000 0 481 +474. 1000 0 481 +475. 1000 0 482 +476. 1000 0 482 +477. 1000 0 482 +478. 1000 0 483 +479. 1000 0 483 +480. 1000 0 483 +481. 1000 0 484 +482. 1000 0 484 +483. 1000 0 484 +484. 1000 0 485 +485. 1000 0 485 +486. 1000 0 485 +487. 1000 0 485 +488. 1000 0 486 +489. 1000 0 486 +490. 1000 0 486 +491. 1000 0 487 +492. 1000 0 487 +493. 1000 0 487 +494. 1000 0 487 +495. 1000 0 488 +496. 1000 0 488 +497. 1000 0 488 +498. 1000 0 489 +499. 1000 0 489 +500. 1000 0 489 +501. 1000 0 489 +502. 1000 0 490 +503. 1000 0 490 +504. 1000 0 490 +505. 1000 0 490 +506. 1000 0 491 +507. 1000 0 491 +508. 1000 0 491 +509. 1000 0 492 +510. 1000 0 492 +511. 1000 0 492 +512. 1000 0 492 +513. 1000 0 493 +514. 1000 0 493 +515. 1000 0 493 +516. 1000 0 493 +517. 1000 0 494 +518. 1000 0 494 +519. 1000 0 494 +520. 1000 0 494 +521. 1000 0 495 +522. 1000 0 495 +523. 1000 0 495 +524. 1000 0 495 +525. 1000 0 496 +526. 1000 0 496 +527. 1000 0 496 +528. 1000 0 496 +529. 1000 0 496 +530. 1000 0 497 +531. 1000 0 497 +532. 1000 0 497 +533. 1000 0 497 +534. 1000 0 498 +535. 1000 0 498 +536. 1000 0 498 +537. 1000 0 498 +538. 1000 0 498 +539. 1000 0 499 +540. 1000 0 499 +541. 1000 0 499 +542. 1000 0 499 +543. 1000 0 500 +544. 1000 0 500 +545. 1000 0 500 +546. 1000 0 500 +547. 1000 0 500 +548. 1000 0 501 +549. 1000 0 501 +550. 1000 0 501 +551. 1000 0 501 +552. 1000 0 501 +553. 1000 0 502 +554. 1000 0 502 +555. 1000 0 502 +556. 1000 0 502 +557. 1000 0 502 +558. 1000 0 503 +559. 1000 0 503 +560. 1000 0 503 +561. 1000 0 503 +562. 1000 0 503 +563. 1000 0 504 +564. 1000 0 504 +565. 1000 0 504 +566. 1000 0 504 +567. 1000 0 504 +568. 1000 0 505 +569. 1000 0 505 +570. 1000 0 505 +571. 1000 0 505 +572. 1000 0 505 +573. 1000 0 506 +574. 1000 0 506 +575. 1000 0 506 +576. 1000 0 506 +577. 1000 0 506 +578. 1000 0 506 +579. 1000 0 507 +580. 1000 0 507 +581. 1000 0 507 +582. 1000 0 507 +583. 1000 0 507 +584. 1000 0 507 +585. 1000 0 508 +586. 1000 0 508 +587. 1000 0 508 +588. 1000 0 508 +589. 1000 0 508 +590. 1000 0 508 +591. 1000 0 509 +592. 1000 0 509 +593. 1000 0 509 +594. 1000 0 509 +595. 1000 0 509 +596. 1000 0 509 +597. 1000 0 510 +598. 1000 0 510 +599. 1000 0 510 +600. 1000 0 510 +601. 1000 0 510 +602. 1000 0 510 +603. 1000 0 511 +604. 1000 0 511 +605. 1000 0 511 +606. 1000 0 511 +607. 1000 0 511 +608. 1000 0 511 +609. 1000 0 511 +610. 1000 0 512 +611. 1000 0 512 +612. 1000 0 512 +613. 1000 0 512 +614. 1000 0 512 +615. 1000 0 512 +616. 1000 0 512 +617. 1000 0 513 +618. 1000 0 513 +619. 1000 0 513 +620. 1000 0 513 +621. 1000 0 513 +622. 1000 0 513 +623. 1000 0 513 +624. 1000 0 514 +625. 1000 0 514 +626. 1000 0 514 +627. 1000 0 514 +628. 1000 0 514 +629. 1000 0 514 +630. 1000 0 514 +631. 1000 0 515 +632. 1000 0 515 +633. 1000 0 515 +634. 1000 0 515 +635. 1000 0 515 +636. 1000 0 515 +637. 1000 0 515 +638. 1000 0 515 +639. 1000 0 516 +640. 1000 0 516 +641. 1000 0 516 +642. 1000 0 516 +643. 1000 0 516 +644. 1000 0 516 +645. 1000 0 516 +646. 1000 0 516 +647. 1000 0 517 +648. 1000 0 517 +649. 1000 0 517 +650. 1000 0 517 +651. 1000 0 517 +652. 1000 0 517 +653. 1000 0 517 +654. 1000 0 517 +655. 1000 0 517 +656. 1000 0 518 +657. 1000 0 518 +658. 1000 0 518 +659. 1000 0 518 +660. 1000 0 518 +661. 1000 0 518 +662. 1000 0 518 +663. 1000 0 518 +664. 1000 0 518 +665. 1000 0 519 +666. 1000 0 519 +667. 1000 0 519 +668. 1000 0 519 +669. 1000 0 519 +670. 1000 0 519 +671. 1000 0 519 +672. 1000 0 519 +673. 1000 0 519 +674. 1000 0 519 +675. 1000 0 520 +676. 1000 0 520 +677. 1000 0 520 +678. 1000 0 520 +679. 1000 0 520 +680. 1000 0 520 +681. 1000 0 520 +682. 1000 0 520 +683. 1000 0 520 +684. 1000 0 520 +685. 1000 0 521 +686. 1000 0 521 +687. 1000 0 521 +688. 1000 0 521 +689. 1000 0 521 +690. 1000 0 521 +691. 1000 0 521 +692. 1000 0 521 +693. 1000 0 521 +694. 1000 0 521 +695. 1000 0 522 +696. 1000 0 522 +697. 1000 0 522 +698. 1000 0 522 +699. 1000 0 522 +700. 1000 0 522 +701. 1000 0 522 +702. 1000 0 522 +703. 1000 0 522 +704. 1000 0 522 +705. 1000 0 522 +706. 1000 0 522 +707. 1000 0 523 +708. 1000 0 523 +709. 1000 0 523 +710. 1000 0 523 +711. 1000 0 523 +712. 1000 0 523 +713. 1000 0 523 +714. 1000 0 523 +715. 1000 0 523 +716. 1000 0 523 +717. 1000 0 523 +718. 1000 0 523 +719. 1000 0 524 +720. 1000 0 524 +721. 1000 0 524 +722. 1000 0 524 +723. 1000 0 524 +724. 1000 0 524 +725. 1000 0 524 +726. 1000 0 524 +727. 1000 0 524 +728. 1000 0 524 +729. 1000 0 524 +730. 1000 0 524 +731. 1000 0 524 +732. 1000 0 524 +733. 1000 0 525 +734. 1000 0 525 +735. 1000 0 525 +736. 1000 0 525 +737. 1000 0 525 +738. 1000 0 525 +739. 1000 0 525 +740. 1000 0 525 +741. 1000 0 525 +742. 1000 0 525 +743. 1000 0 525 +744. 1000 0 525 +745. 1000 0 525 +746. 1000 0 525 +747. 1000 0 526 +748. 1000 0 526 +749. 1000 0 526 +750. 1000 0 526 +751. 1000 0 526 +752. 1000 0 526 +753. 1000 0 526 +754. 1000 0 526 +755. 1000 0 526 +756. 1000 0 526 +757. 1000 0 526 +758. 1000 0 526 +759. 1000 0 526 +760. 1000 0 526 +761. 1000 0 526 +762. 1000 0 526 +763. 1000 0 527 +764. 1000 0 527 +765. 1000 0 527 +766. 1000 0 527 +767. 1000 0 527 +768. 1000 0 527 +769. 1000 0 527 +770. 1000 0 527 +771. 1000 0 527 +772. 1000 0 527 +773. 1000 0 527 +774. 1000 0 527 +775. 1000 0 527 +776. 1000 0 527 +777. 1000 0 527 +778. 1000 0 527 +779. 1000 0 527 +780. 1000 0 528 +781. 1000 0 528 +782. 1000 0 528 +783. 1000 0 528 +784. 1000 0 528 +785. 1000 0 528 +786. 1000 0 528 +787. 1000 0 528 +788. 1000 0 528 +789. 1000 0 528 +790. 1000 0 528 +791. 1000 0 528 +792. 1000 0 528 +793. 1000 0 528 +794. 1000 0 528 +795. 1000 0 528 +796. 1000 0 528 +797. 1000 0 528 +798. 1000 0 528 +799. 1000 0 529 +800. 1000 0 529 +801. 1000 0 529 +802. 1000 0 529 +803. 1000 0 529 +804. 1000 0 529 +805. 1000 0 529 +806. 1000 0 529 +807. 1000 0 529 +808. 1000 0 529 +809. 1000 0 529 +810. 1000 0 529 +811. 1000 0 529 +812. 1000 0 529 +813. 1000 0 529 +814. 1000 0 529 +815. 1000 0 529 +816. 1000 0 529 +817. 1000 0 529 +818. 1000 0 529 +819. 1000 0 529 +820. 1000 0 529 +821. 1000 0 530 +822. 1000 0 530 +823. 1000 0 530 +824. 1000 0 530 +825. 1000 0 530 +826. 1000 0 530 +827. 1000 0 530 +828. 1000 0 530 +829. 1000 0 530 +830. 1000 0 530 +831. 1000 0 530 +832. 1000 0 530 +833. 1000 0 530 +834. 1000 0 530 +835. 1000 0 530 +836. 1000 0 530 +837. 1000 0 530 +838. 1000 0 530 +839. 1000 0 530 +840. 1000 0 530 +841. 1000 0 530 +842. 1000 0 530 +843. 1000 0 530 +844. 1000 0 530 +845. 1000 0 530 +846. 1000 0 531 +847. 1000 0 531 +848. 1000 0 531 +849. 1000 0 531 +850. 1000 0 531 +851. 1000 0 531 +852. 1000 0 531 +853. 1000 0 531 +854. 1000 0 531 +855. 1000 0 531 +856. 1000 0 531 +857. 1000 0 531 +858. 1000 0 531 +859. 1000 0 531 +860. 1000 0 531 +861. 1000 0 531 +862. 1000 0 531 +863. 1000 0 531 +864. 1000 0 531 +865. 1000 0 531 +866. 1000 0 531 +867. 1000 0 531 +868. 1000 0 531 +869. 1000 0 531 +870. 1000 0 531 +871. 1000 0 531 +872. 1000 0 531 +873. 1000 0 531 +874. 1000 0 531 +875. 1000 0 531 +876. 1000 0 532 +877. 1000 0 532 +878. 1000 0 532 +879. 1000 0 532 +880. 1000 0 532 +881. 1000 0 532 +882. 1000 0 532 +883. 1000 0 532 +884. 1000 0 532 +885. 1000 0 532 +886. 1000 0 532 +887. 1000 0 532 +888. 1000 0 532 +889. 1000 0 532 +890. 1000 0 532 +891. 1000 0 532 +892. 1000 0 532 +893. 1000 0 532 +894. 1000 0 532 +895. 1000 0 532 +896. 1000 0 532 +897. 1000 0 532 +898. 1000 0 532 +899. 1000 0 532 +900. 1000 0 532 +901. 1000 0 532 +902. 1000 0 532 +903. 1000 0 532 +904. 1000 0 532 +905. 1000 0 532 +906. 1000 0 532 +907. 1000 0 532 +908. 1000 0 532 +909. 1000 0 532 +910. 1000 0 532 +911. 1000 0 532 +912. 1000 0 533 +913. 1000 0 533 +914. 1000 0 533 +915. 1000 0 533 +916. 1000 0 533 +917. 1000 0 533 +918. 1000 0 533 +919. 1000 0 533 +920. 1000 0 533 +921. 1000 0 533 +922. 1000 0 533 +923. 1000 0 533 +924. 1000 0 533 +925. 1000 0 533 +926. 1000 0 533 +927. 1000 0 533 +928. 1000 0 533 +929. 1000 0 533 +930. 1000 0 533 +931. 1000 0 533 +932. 1000 0 533 +933. 1000 0 533 +934. 1000 0 533 +935. 1000 0 533 +936. 1000 0 533 +937. 1000 0 533 +938. 1000 0 533 +939. 1000 0 533 +940. 1000 0 533 +941. 1000 0 533 +942. 1000 0 533 +943. 1000 0 533 +944. 1000 0 533 +945. 1000 0 533 +946. 1000 0 533 +947. 1000 0 533 +948. 1000 0 533 +949. 1000 0 533 +950. 1000 0 533 +951. 1000 0 533 +952. 1000 0 533 +953. 1000 0 533 +954. 1000 0 533 +955. 1000 0 533 +956. 1000 0 533 +957. 1000 0 534 +958. 1000 0 534 +959. 1000 0 534 +960. 1000 0 534 +961. 1000 0 534 +962. 1000 0 534 +963. 1000 0 534 +964. 1000 0 534 +965. 1000 0 534 +966. 1000 0 534 +967. 1000 0 534 +968. 1000 0 534 +969. 1000 0 534 +970. 1000 0 534 +971. 1000 0 534 +972. 1000 0 534 +973. 1000 0 534 +974. 1000 0 534 +975. 1000 0 534 +976. 1000 0 534 +977. 1000 0 534 +978. 1000 0 534 +979. 1000 0 534 +980. 1000 0 534 +981. 1000 0 534 +982. 1000 0 534 +983. 1000 0 534 +984. 1000 0 534 +985. 1000 0 534 +986. 1000 0 534 +987. 1000 0 534 +988. 1000 0 534 +989. 1000 0 534 +990. 1000 0 534 +991. 1000 0 534 +992. 1000 0 534 +993. 1000 0 534 +994. 1000 0 534 +995. 1000 0 534 +996. 1000 0 534 +997. 1000 0 534 +998. 1000 0 534 +999. 1000 0 534 +1000. 1000 0 534 +1001. 1000 0 534 +1002. 1000 0 534 +1003. 1000 0 534 +1004. 1000 0 534 +1005. 1000 0 534 +1006. 1000 0 534 +1007. 1000 0 534 +1008. 1000 0 534 +1009. 1000 0 534 +1010. 1000 0 534 +1011. 1000 0 534 +1012. 1000 0 534 +1013. 1000 0 534 +1014. 1000 0 534 +1015. 1000 0 534 +1016. 1000 0 534 +1017. 1000 0 534 +1018. 1000 0 534 +1019. 1000 0 534 +1020. 1000 0 535 +1021. 1000 0 535 +1022. 1000 0 535 +1023. 1000 0 535 +1024. 1000 0 535 +1025. 1000 0 535 +1026. 1000 0 535 +1027. 1000 0 535 +1028. 1000 0 535 +1029. 1000 0 535 +1030. 1000 0 535 +1031. 1000 0 535 +1032. 1000 0 535 +1033. 1000 0 535 +1034. 1000 0 535 +1035. 1000 0 535 +1036. 1000 0 535 +1037. 1000 0 535 +1038. 1000 0 535 +1039. 1000 0 535 +1040. 1000 0 535 +1041. 1000 0 535 +1042. 1000 0 535 +1043. 1000 0 535 +1044. 1000 0 535 +1045. 1000 0 535 +1046. 1000 0 535 +1047. 1000 0 535 +1048. 1000 0 535 +1049. 1000 0 535 +1050. 1000 0 535 +1051. 1000 0 535 +1052. 1000 0 535 +1053. 1000 0 535 +1054. 1000 0 535 +1055. 1000 0 535 +1056. 1000 0 535 +1057. 1000 0 535 +1058. 1000 0 535 +1059. 1000 0 535 +1060. 1000 0 535 +1061. 1000 0 535 +1062. 1000 0 535 +1063. 1000 0 535 +1064. 1000 0 535 +1065. 1000 0 535 +1066. 1000 0 535 +1067. 1000 0 535 +1068. 1000 0 535 +1069. 1000 0 535 +1070. 1000 0 535 +1071. 1000 0 535 +1072. 1000 0 535 +1073. 1000 0 535 +1074. 1000 0 535 +1075. 1000 0 535 +1076. 1000 0 535 +1077. 1000 0 535 +1078. 1000 0 535 +1079. 1000 0 535 +1080. 1000 0 535 +1081. 1000 0 535 +1082. 1000 0 535 +1083. 1000 0 535 +1084. 1000 0 535 +1085. 1000 0 535 +1086. 1000 0 535 +1087. 1000 0 535 +1088. 1000 0 535 +1089. 1000 0 535 +1090. 1000 0 535 +1091. 1000 0 535 +1092. 1000 0 535 +1093. 1000 0 535 +1094. 1000 0 535 +1095. 1000 0 535 +1096. 1000 0 535 +1097. 1000 0 535 +1098. 1000 0 535 +1099. 1000 0 535 +1100. 1000 0 535 +1101. 1000 0 535 +1102. 1000 0 535 +1103. 1000 0 535 +1104. 1000 0 535 +1105. 1000 0 535 +1106. 1000 0 535 +1107. 1000 0 535 +1108. 1000 0 535 +1109. 1000 0 535 +1110. 1000 0 535 +1111. 1000 0 535 +1112. 1000 0 535 +1113. 1000 0 535 +1114. 1000 0 535 +1115. 1000 0 535 +1116. 1000 0 535 +1117. 1000 0 535 +1118. 1000 0 535 +1119. 1000 0 535 +1120. 1000 0 535 +1121. 1000 0 535 +1122. 1000 0 536 +1123. 1000 0 536 +1124. 1000 0 536 +1125. 1000 0 536 +1126. 1000 0 536 +1127. 1000 0 536 +1128. 1000 0 536 +1129. 1000 0 536 +1130. 1000 0 536 +1131. 1000 0 536 +1132. 1000 0 536 +1133. 1000 0 536 +1134. 1000 0 536 +1135. 1000 0 536 +1136. 1000 0 536 +1137. 1000 0 536 +1138. 1000 0 536 +1139. 1000 0 536 +1140. 1000 0 536 +1141. 1000 0 536 +1142. 1000 0 536 +1143. 1000 0 536 +1144. 1000 0 536 +1145. 1000 0 536 +1146. 1000 0 536 +1147. 1000 0 536 +1148. 1000 0 536 +1149. 1000 0 536 +1150. 1000 0 536 +1151. 1000 0 536 +1152. 1000 0 536 +1153. 1000 0 536 +1154. 1000 0 536 +1155. 1000 0 536 +1156. 1000 0 536 +1157. 1000 0 536 +1158. 1000 0 536 +1159. 1000 0 536 +1160. 1000 0 536 +1161. 1000 0 536 +1162. 1000 0 536 +1163. 1000 0 536 +1164. 1000 0 536 +1165. 1000 0 536 +1166. 1000 0 536 +1167. 1000 0 536 +1168. 1000 0 536 +1169. 1000 0 536 +1170. 1000 0 536 +1171. 1000 0 536 +1172. 1000 0 536 +1173. 1000 0 536 +1174. 1000 0 536 +1175. 1000 0 536 +1176. 1000 0 536 +1177. 1000 0 536 +1178. 1000 0 536 +1179. 1000 0 536 +1180. 1000 0 536 +1181. 1000 0 536 +1182. 1000 0 536 +1183. 1000 0 536 +1184. 1000 0 536 +1185. 1000 0 536 +1186. 1000 0 536 +1187. 1000 0 536 +1188. 1000 0 536 +1189. 1000 0 536 +1190. 1000 0 536 +1191. 1000 0 536 +1192. 1000 0 536 +1193. 1000 0 536 +1194. 1000 0 536 +1195. 1000 0 536 +1196. 1000 0 536 +1197. 1000 0 536 +1198. 1000 0 536 +1199. 1000 0 536 +1200. 1000 0 536 +1201. 1000 0 536 +1202. 1000 0 536 +1203. 1000 0 536 +1204. 1000 0 536 +1205. 1000 0 536 +1206. 1000 0 536 +1207. 1000 0 536 +1208. 1000 0 536 +1209. 1000 0 536 +1210. 1000 0 536 +1211. 1000 0 536 +1212. 1000 0 536 +1213. 1000 0 536 +1214. 1000 0 536 +1215. 1000 0 536 +1216. 1000 0 536 +1217. 1000 0 536 +1218. 1000 0 536 +1219. 1000 0 536 +1220. 1000 0 536 +1221. 1000 0 536 +1222. 1000 0 536 +1223. 1000 0 536 +1224. 1000 0 536 +1225. 1000 0 536 +1226. 1000 0 536 +1227. 1000 0 536 +1228. 1000 0 536 +1229. 1000 0 536 +1230. 1000 0 536 +1231. 1000 0 536 +1232. 1000 0 536 +1233. 1000 0 536 +1234. 1000 0 536 +1235. 1000 0 536 +1236. 1000 0 536 +1237. 1000 0 536 +1238. 1000 0 536 +1239. 1000 0 536 +1240. 1000 0 536 +1241. 1000 0 536 +1242. 1000 0 536 +1243. 1000 0 536 +1244. 1000 0 536 +1245. 1000 0 536 +1246. 1000 0 536 +1247. 1000 0 536 +1248. 1000 0 536 +1249. 1000 0 536 +1250. 1000 0 536 +1251. 1000 0 536 +1252. 1000 0 536 +1253. 1000 0 536 +1254. 1000 0 536 +1255. 1000 0 536 +1256. 1000 0 536 +1257. 1000 0 536 +1258. 1000 0 536 +1259. 1000 0 536 +1260. 1000 0 536 +1261. 1000 0 536 +1262. 1000 0 536 +1263. 1000 0 536 +1264. 1000 0 536 +1265. 1000 0 536 +1266. 1000 0 536 +1267. 1000 0 536 +1268. 1000 0 536 +1269. 1000 0 536 +1270. 1000 0 536 +1271. 1000 0 536 +1272. 1000 0 536 +1273. 1000 0 536 +1274. 1000 0 536 +1275. 1000 0 536 +1276. 1000 0 536 +1277. 1000 0 536 +1278. 1000 0 536 +1279. 1000 0 536 +1280. 1000 0 536 +1281. 1000 0 536 +1282. 1000 0 536 +1283. 1000 0 536 +1284. 1000 0 536 +1285. 1000 0 536 +1286. 1000 0 536 +1287. 1000 0 536 +1288. 1000 0 536 +1289. 1000 0 536 +1290. 1000 0 536 +1291. 1000 0 536 +1292. 1000 0 536 +1293. 1000 0 536 +1294. 1000 0 536 +1295. 1000 0 536 +1296. 1000 0 536 +1297. 1000 0 536 +1298. 1000 0 536 +1299. 1000 0 536 +1300. 1000 0 536 +1301. 1000 0 536 +1302. 1000 0 536 +1303. 1000 0 536 +1304. 1000 0 536 +1305. 1000 0 536 +1306. 1000 0 536 +1307. 1000 0 536 +1308. 1000 0 536 +1309. 1000 0 536 +1310. 1000 0 536 +1311. 1000 0 536 +1312. 1000 0 536 +1313. 1000 0 536 +1314. 1000 0 536 +1315. 1000 0 536 +1316. 1000 0 536 +1317. 1000 0 536 +1318. 1000 0 536 +1319. 1000 0 536 +1320. 1000 0 536 +1321. 1000 0 536 +1322. 1000 0 536 +1323. 1000 0 536 +1324. 1000 0 536 +1325. 1000 0 536 +1326. 1000 0 536 +1327. 1000 0 536 +1328. 1000 0 536 +1329. 1000 0 536 +1330. 1000 0 536 +1331. 1000 0 536 +1332. 1000 0 536 +1333. 1000 0 536 +1334. 1000 0 536 +1335. 1000 0 536 +1336. 1000 0 536 +1337. 1000 0 536 +1338. 1000 0 536 +1339. 1000 0 536 +1340. 1000 0 536 +1341. 1000 0 536 +1342. 1000 0 536 +1343. 1000 0 536 +1344. 1000 0 536 +1345. 1000 0 536 +1346. 1000 0 536 +1347. 1000 0 536 +1348. 1000 0 536 +1349. 1000 0 536 +1350. 1000 0 536 +1351. 1000 0 536 +1352. 1000 0 536 +1353. 1000 0 536 +1354. 1000 0 536 +1355. 1000 0 536 +1356. 1000 0 536 +1357. 1000 0 536 +1358. 1000 0 536 +1359. 1000 0 536 +1360. 1000 0 536 +1361. 1000 0 536 +1362. 1000 0 536 +1363. 1000 0 536 +1364. 1000 0 536 +1365. 1000 0 536 +1366. 1000 0 536 +1367. 1000 0 536 +1368. 1000 0 536 +1369. 1000 0 536 +1370. 1000 0 536 +1371. 1000 0 536 +1372. 1000 0 536 +1373. 1000 0 536 +1374. 1000 0 536 +1375. 1000 0 536 +1376. 1000 0 536 +1377. 1000 0 536 +1378. 1000 0 536 +1379. 1000 0 536 +1380. 1000 0 536 +1381. 1000 0 536 +1382. 1000 0 536 +1383. 1000 0 536 +1384. 1000 0 536 +1385. 1000 0 536 +1386. 1000 0 536 +1387. 1000 0 536 +1388. 1000 0 536 +1389. 1000 0 536 +1390. 1000 0 536 +1391. 1000 0 536 +1392. 1000 0 536 +1393. 1000 0 536 +1394. 1000 0 536 +1395. 1000 0 536 +1396. 1000 0 536 +1397. 1000 0 536 +1398. 1000 0 536 +1399. 1000 0 536 +1400. 1000 0 536 +1401. 1000 0 536 +1402. 1000 0 536 +1403. 1000 0 536 +1404. 1000 0 536 +1405. 1000 0 536 +1406. 1000 0 536 +1407. 1000 0 536 +1408. 1000 0 536 +1409. 1000 0 536 +1410. 1000 0 536 +1411. 1000 0 536 +1412. 1000 0 536 +1413. 1000 0 536 +1414. 1000 0 536 +1415. 1000 0 536 +1416. 1000 0 536 +1417. 1000 0 536 +1418. 1000 0 536 +1419. 1000 0 536 +1420. 1000 0 536 +1421. 1000 0 536 +1422. 1000 0 536 +1423. 1000 0 536 +1424. 1000 0 536 +1425. 1000 0 536 +1426. 1000 0 536 +1427. 1000 0 536 +1428. 1000 0 536 +1429. 1000 0 536 +1430. 1000 0 536 +1431. 1000 0 537 +1432. 1000 0 537 +1433. 1000 0 537 +1434. 1000 0 537 +1435. 1000 0 537 +1436. 1000 0 537 +1437. 1000 0 537 +1438. 1000 0 537 +1439. 1000 0 537 +1440. 1000 0 537 +1441. 1000 0 537 +1442. 1000 0 537 +1443. 1000 0 537 +1444. 1000 0 537 +1445. 1000 0 537 +1446. 1000 0 537 +1447. 1000 0 537 +1448. 1000 0 537 +1449. 1000 0 537 +1450. 1000 0 537 +1451. 1000 0 537 +1452. 1000 0 537 +1453. 1000 0 537 +1454. 1000 0 537 +1455. 1000 0 537 +1456. 1000 0 537 +1457. 1000 0 537 +1458. 1000 0 537 +1459. 1000 0 537 +1460. 1000 0 537 +1461. 1000 0 537 +1462. 1000 0 537 +1463. 1000 0 537 +1464. 1000 0 537 +1465. 1000 0 537 +1466. 1000 0 537 +1467. 1000 0 537 +1468. 1000 0 537 +1469. 1000 0 537 +1470. 1000 0 537 +1471. 1000 0 537 +1472. 1000 0 537 +1473. 1000 0 537 +1474. 1000 0 537 +1475. 1000 0 537 +1476. 1000 0 537 +1477. 1000 0 537 +1478. 1000 0 537 +1479. 1000 0 537 +1480. 1000 0 537 +1481. 1000 0 537 +1482. 1000 0 537 +1483. 1000 0 537 +1484. 1000 0 537 +1485. 1000 0 537 +1486. 1000 0 537 +1487. 1000 0 537 +1488. 1000 0 537 +1489. 1000 0 537 +1490. 1000 0 537 +1491. 1000 0 537 +1492. 1000 0 537 +1493. 1000 0 537 +1494. 1000 0 537 +1495. 1000 0 537 +1496. 1000 0 537 +1497. 1000 0 537 +1498. 1000 0 537 +1499. 1000 0 537 +1500. 1000 0 537 +1501. 1000 0 537 +1502. 1000 0 537 +1503. 1000 0 537 +1504. 1000 0 537 +1505. 1000 0 537 +1506. 1000 0 537 +1507. 1000 0 537 +1508. 1000 0 537 +1509. 1000 0 537 +1510. 1000 0 537 +1511. 1000 0 537 +1512. 1000 0 537 +1513. 1000 0 537 +1514. 1000 0 537 +1515. 1000 0 537 +1516. 1000 0 537 +1517. 1000 0 537 +1518. 1000 0 537 +1519. 1000 0 537 +1520. 1000 0 537 +1521. 1000 0 537 +1522. 1000 0 537 +1523. 1000 0 537 +1524. 1000 0 537 +1525. 1000 0 537 +1526. 1000 0 537 +1527. 1000 0 537 +1528. 1000 0 537 +1529. 1000 0 537 +1530. 1000 0 537 +1531. 1000 0 537 +1532. 1000 0 537 +1533. 1000 0 537 +1534. 1000 0 537 +1535. 1000 0 537 +1536. 1000 0 537 +1537. 1000 0 537 +1538. 1000 0 537 +1539. 1000 0 537 +1540. 1000 0 537 +1541. 1000 0 537 +1542. 1000 0 537 +1543. 1000 0 537 +1544. 1000 0 537 +1545. 1000 0 537 +1546. 1000 0 537 +1547. 1000 0 537 +1548. 1000 0 537 +1549. 1000 0 537 +1550. 1000 0 537 +1551. 1000 0 537 +1552. 1000 0 537 +1553. 1000 0 537 +1554. 1000 0 537 +1555. 1000 0 537 +1556. 1000 0 537 +1557. 1000 0 537 +1558. 1000 0 537 +1559. 1000 0 537 +1560. 1000 0 537 +1561. 1000 0 537 +1562. 1000 0 537 +1563. 1000 0 537 +1564. 1000 0 537 +1565. 1000 0 537 +1566. 1000 0 537 +1567. 1000 0 537 +1568. 1000 0 537 +1569. 1000 0 537 +1570. 1000 0 537 +1571. 1000 0 537 +1572. 1000 0 537 +1573. 1000 0 537 +1574. 1000 0 537 +1575. 1000 0 537 +1576. 1000 0 537 +1577. 1000 0 537 +1578. 1000 0 537 +1579. 1000 0 537 +1580. 1000 0 537 +1581. 1000 0 537 +1582. 1000 0 537 +1583. 1000 0 537 +1584. 1000 0 537 +1585. 1000 0 537 +1586. 1000 0 537 +1587. 1000 0 537 +1588. 1000 0 537 +1589. 1000 0 537 +1590. 1000 0 537 +1591. 1000 0 537 +1592. 1000 0 537 +1593. 1000 0 537 +1594. 1000 0 537 +1595. 1000 0 537 +1596. 1000 0 537 +1597. 1000 0 537 +1598. 1000 0 537 +1599. 1000 0 537 +1600. 1000 0 537 +1601. 1000 0 537 +1602. 1000 0 537 +1603. 1000 0 537 +1604. 1000 0 537 +1605. 1000 0 537 +1606. 1000 0 537 +1607. 1000 0 537 +1608. 1000 0 537 +1609. 1000 0 537 +1610. 1000 0 537 +1611. 1000 0 537 +1612. 1000 0 537 +1613. 1000 0 537 +1614. 1000 0 537 +1615. 1000 0 537 +1616. 1000 0 537 +1617. 1000 0 537 +1618. 1000 0 537 +1619. 1000 0 537 +1620. 1000 0 537 +1621. 1000 0 537 +1622. 1000 0 537 +1623. 1000 0 537 +1624. 1000 0 537 +1625. 1000 0 537 +1626. 1000 0 537 +1627. 1000 0 537 +1628. 1000 0 537 +1629. 1000 0 537 +1630. 1000 0 537 +1631. 1000 0 537 +1632. 1000 0 537 +1633. 1000 0 537 +1634. 1000 0 537 +1635. 1000 0 537 +1636. 1000 0 537 +1637. 1000 0 537 +1638. 1000 0 537 +1639. 1000 0 537 +1640. 1000 0 537 +1641. 1000 0 537 +1642. 1000 0 537 +1643. 1000 0 537 +1644. 1000 0 537 +1645. 1000 0 537 +1646. 1000 0 537 +1647. 1000 0 537 +1648. 1000 0 537 +1649. 1000 0 537 +1650. 1000 0 537 +1651. 1000 0 537 +1652. 1000 0 537 +1653. 1000 0 537 +1654. 1000 0 537 +1655. 1000 0 537 +1656. 1000 0 537 +1657. 1000 0 537 +1658. 1000 0 537 +1659. 1000 0 537 +1660. 1000 0 537 +1661. 1000 0 537 +1662. 1000 0 537 +1663. 1000 0 537 +1664. 1000 0 537 +1665. 1000 0 537 +1666. 1000 0 537 +1667. 1000 0 537 +1668. 1000 0 537 +1669. 1000 0 537 +1670. 1000 0 537 +1671. 1000 0 537 +1672. 1000 0 537 +1673. 1000 0 537 +1674. 1000 0 537 +1675. 1000 0 537 +1676. 1000 0 537 +1677. 1000 0 537 +1678. 1000 0 537 +1679. 1000 0 537 +1680. 1000 0 537 +1681. 1000 0 537 +1682. 1000 0 537 +1683. 1000 0 537 +1684. 1000 0 537 +1685. 1000 0 537 +1686. 1000 0 537 +1687. 1000 0 537 +1688. 1000 0 537 +1689. 1000 0 537 +1690. 1000 0 537 +1691. 1000 0 537 +1692. 1000 0 537 +1693. 1000 0 537 +1694. 1000 0 537 +1695. 1000 0 537 +1696. 1000 0 537 +1697. 1000 0 537 +1698. 1000 0 537 +1699. 1000 0 537 +1700. 1000 0 537 +1701. 1000 0 537 +1702. 1000 0 537 +1703. 1000 0 537 +1704. 1000 0 537 +1705. 1000 0 537 +1706. 1000 0 537 +1707. 1000 0 537 +1708. 1000 0 537 +1709. 1000 0 537 +1710. 1000 0 537 +1711. 1000 0 537 +1712. 1000 0 537 +1713. 1000 0 537 +1714. 1000 0 537 +1715. 1000 0 537 +1716. 1000 0 537 +1717. 1000 0 537 +1718. 1000 0 537 +1719. 1000 0 537 +1720. 1000 0 537 +1721. 1000 0 537 +1722. 1000 0 537 +1723. 1000 0 537 +1724. 1000 0 537 +1725. 1000 0 537 +1726. 1000 0 537 +1727. 1000 0 537 +1728. 1000 0 537 +1729. 1000 0 537 +1730. 1000 0 537 +1731. 1000 0 537 +1732. 1000 0 537 +1733. 1000 0 537 +1734. 1000 0 537 +1735. 1000 0 537 +1736. 1000 0 537 +1737. 1000 0 537 +1738. 1000 0 537 +1739. 1000 0 537 +1740. 1000 0 537 +1741. 1000 0 537 +1742. 1000 0 537 +1743. 1000 0 537 +1744. 1000 0 537 +1745. 1000 0 537 +1746. 1000 0 537 +1747. 1000 0 537 +1748. 1000 0 537 +1749. 1000 0 537 +1750. 1000 0 537 +1751. 1000 0 537 +1752. 1000 0 537 +1753. 1000 0 537 +1754. 1000 0 537 +1755. 1000 0 537 +1756. 1000 0 537 +1757. 1000 0 537 +1758. 1000 0 537 +1759. 1000 0 537 +1760. 1000 0 537 +1761. 1000 0 537 +1762. 1000 0 537 +1763. 1000 0 537 +1764. 1000 0 537 +1765. 1000 0 537 +1766. 1000 0 537 +1767. 1000 0 537 +1768. 1000 0 537 +1769. 1000 0 537 +1770. 1000 0 537 +1771. 1000 0 537 +1772. 1000 0 537 +1773. 1000 0 537 +1774. 1000 0 537 +1775. 1000 0 537 +1776. 1000 0 537 +1777. 1000 0 537 +1778. 1000 0 537 +1779. 1000 0 537 +1780. 1000 0 537 +1781. 1000 0 537 +1782. 1000 0 537 +1783. 1000 0 537 +1784. 1000 0 537 +1785. 1000 0 537 +1786. 1000 0 537 +1787. 1000 0 537 +1788. 1000 0 537 +1789. 1000 0 537 +1790. 1000 0 537 +1791. 1000 0 537 +1792. 1000 0 537 +1793. 1000 0 537 +1794. 1000 0 537 +1795. 1000 0 537 +1796. 1000 0 537 +1797. 1000 0 537 +1798. 1000 0 537 +1799. 1000 0 537 +1800. 1000 0 537 +1801. 1000 0 537 +1802. 1000 0 537 +1803. 1000 0 537 +1804. 1000 0 537 +1805. 1000 0 537 +1806. 1000 0 537 +1807. 1000 0 537 +1808. 1000 0 537 +1809. 1000 0 537 +1810. 1000 0 537 +1811. 1000 0 537 +1812. 1000 0 537 +1813. 1000 0 537 +1814. 1000 0 537 +1815. 1000 0 537 +1816. 1000 0 537 +1817. 1000 0 537 +1818. 1000 0 537 +1819. 1000 0 537 +1820. 1000 0 537 +1821. 1000 0 537 +1822. 1000 0 537 +1823. 1000 0 537 +1824. 1000 0 537 +1825. 1000 0 537 +1826. 1000 0 537 +1827. 1000 0 537 +1828. 1000 0 537 +1829. 1000 0 537 +1830. 1000 0 537 +1831. 1000 0 537 +1832. 1000 0 537 +1833. 1000 0 537 +1834. 1000 0 537 +1835. 1000 0 537 +1836. 1000 0 537 +1837. 1000 0 537 +1838. 1000 0 537 +1839. 1000 0 537 +1840. 1000 0 537 +1841. 1000 0 537 +1842. 1000 0 537 +1843. 1000 0 537 +1844. 1000 0 537 +1845. 1000 0 537 +1846. 1000 0 537 +1847. 1000 0 537 +1848. 1000 0 537 +1849. 1000 0 537 +1850. 1000 0 537 +1851. 1000 0 537 +1852. 1000 0 537 +1853. 1000 0 537 +1854. 1000 0 537 +1855. 1000 0 537 +1856. 1000 0 537 +1857. 1000 0 537 +1858. 1000 0 537 +1859. 1000 0 537 +1860. 1000 0 537 +1861. 1000 0 537 +1862. 1000 0 537 +1863. 1000 0 537 +1864. 1000 0 537 +1865. 1000 0 537 +1866. 1000 0 537 +1867. 1000 0 537 +1868. 1000 0 537 +1869. 1000 0 537 +1870. 1000 0 537 +1871. 1000 0 537 +1872. 1000 0 537 +1873. 1000 0 537 +1874. 1000 0 537 +1875. 1000 0 537 +1876. 1000 0 537 +1877. 1000 0 537 +1878. 1000 0 537 +1879. 1000 0 537 +1880. 1000 0 537 +1881. 1000 0 537 +1882. 1000 0 537 +1883. 1000 0 537 +1884. 1000 0 537 +1885. 1000 0 537 +1886. 1000 0 537 +1887. 1000 0 537 +1888. 1000 0 537 +1889. 1000 0 537 +1890. 1000 0 537 +1891. 1000 0 537 +1892. 1000 0 537 +1893. 1000 0 537 +1894. 1000 0 537 +1895. 1000 0 537 +1896. 1000 0 537 +1897. 1000 0 537 +1898. 1000 0 537 +1899. 1000 0 537 +1900. 1000 0 537 +1901. 1000 0 537 +1902. 1000 0 537 +1903. 1000 0 537 +1904. 1000 0 537 +1905. 1000 0 537 +1906. 1000 0 537 +1907. 1000 0 537 +1908. 1000 0 537 +1909. 1000 0 537 +1910. 1000 0 537 +1911. 1000 0 537 +1912. 1000 0 537 +1913. 1000 0 537 +1914. 1000 0 537 +1915. 1000 0 537 +1916. 1000 0 537 +1917. 1000 0 537 +1918. 1000 0 537 +1919. 1000 0 537 +1920. 1000 0 537 +1921. 1000 0 537 +1922. 1000 0 537 +1923. 1000 0 537 +1924. 1000 0 537 +1925. 1000 0 537 +1926. 1000 0 537 +1927. 1000 0 537 +1928. 1000 0 537 +1929. 1000 0 537 +1930. 1000 0 537 +1931. 1000 0 537 +1932. 1000 0 537 +1933. 1000 0 537 +1934. 1000 0 537 +1935. 1000 0 537 +1936. 1000 0 537 +1937. 1000 0 537 +1938. 1000 0 537 +1939. 1000 0 537 +1940. 1000 0 537 +1941. 1000 0 537 +1942. 1000 0 537 +1943. 1000 0 537 +1944. 1000 0 537 +1945. 1000 0 537 +1946. 1000 0 537 +1947. 1000 0 537 +1948. 1000 0 537 +1949. 1000 0 537 +1950. 1000 0 537 +1951. 1000 0 537 +1952. 1000 0 537 +1953. 1000 0 537 +1954. 1000 0 537 +1955. 1000 0 537 +1956. 1000 0 537 +1957. 1000 0 537 +1958. 1000 0 537 +1959. 1000 0 537 +1960. 1000 0 537 +1961. 1000 0 537 +1962. 1000 0 537 +1963. 1000 0 537 +1964. 1000 0 537 +1965. 1000 0 537 +1966. 1000 0 537 +1967. 1000 0 537 +1968. 1000 0 537 +1969. 1000 0 537 +1970. 1000 0 537 +1971. 1000 0 537 +1972. 1000 0 537 +1973. 1000 0 537 +1974. 1000 0 537 +1975. 1000 0 537 +1976. 1000 0 537 +1977. 1000 0 537 +1978. 1000 0 537 +1979. 1000 0 537 +1980. 1000 0 537 +1981. 1000 0 537 +1982. 1000 0 537 +1983. 1000 0 537 +1984. 1000 0 537 +1985. 1000 0 537 +1986. 1000 0 537 +1987. 1000 0 537 +1988. 1000 0 537 +1989. 1000 0 537 +1990. 1000 0 537 +1991. 1000 0 537 +1992. 1000 0 537 +1993. 1000 0 537 +1994. 1000 0 537 +1995. 1000 0 537 +1996. 1000 0 537 +1997. 1000 0 537 +1998. 1000 0 537 +1999. 1000 0 537 +2000. 1000 0 537 +2001. 1000 0 537 diff --git a/tests/source/DiffSystem.scade b/tests/source/DiffSystem.scade new file mode 100644 index 0000000..b1f3fb4 --- /dev/null +++ b/tests/source/DiffSystem.scade @@ -0,0 +1,34 @@ + +node Body(Torq, Brake : real) returns (probe VehicleSpeed : real) +var pre_VS, Cmd : real; +let + --assume h1: Brake = 0.; + --assume h2: Torq >= 0. and Torq <= 1.; + + pre_VS = 0.0 -> pre VehicleSpeed; + + Cmd = + (if Torq <= 1.0 then 150.0 else 0.0) + + Brake * 200.0 + + pre_VS * pre_VS * 0.3 + + pre_VS * 2.5; + + VehicleSpeed = + (Torq - (if pre_VS < - 0.1 then - Cmd else if pre_VS > 0.1 then Cmd else 0.0)) + * 0.1 * 2.5 / 1450.0 + + pre_VS; +tel + +node test(i: int) returns(a, b, c: int; exit: bool) +var torq, brake, vs: real; +let + torq = 1000.; --if i mod 311 > 240 then 2.0 else if i mod 211 > 170 then 0.9 else 0.5; + brake = 0.; --if i mod 400 > 300 then 1.4 else 0.; + vs = Body(torq, brake); + + a = int(torq); + b = int(brake); + c = int(vs * 10.); + exit = (i > 2000); +tel + diff --git a/tests/source/NestedControl.scade b/tests/source/NestedControl.scade new file mode 100644 index 0000000..2551eb6 --- /dev/null +++ b/tests/source/NestedControl.scade @@ -0,0 +1,47 @@ +node root(In : int; C : bool) returns (Out, Out1 : int) +var last_Out, last_Out1: int; + isp, isn: bool; +let + last_Out = 0 -> pre Out; + last_Out1 = 0 -> pre Out1; + + isp = In > 0; + isn = In < 0; + assume C_in_not_null: (not C) or isp or isn; + + automaton SM1 + initial state State1 + let + Out1 = 2; + Out = 3; + tel + until + if C resume State2; + + state State2 + let + automaton SM2 + initial state State3 + Out1 = 1; + until + if C resume State4; + + state State4 + activate if C + then let + guarantee no_mod0: Out <> 0; + Out1 = In mod Out; + tel else Out1 = last_Out1; + returns Out1; + + returns Out1; + + activate if C + then Out = In; + else Out = last_Out; + returns Out; + + tel + + returns Out, Out1; +tel diff --git a/tests/source/Overflows.scade b/tests/source/Overflows.scade new file mode 100644 index 0000000..e9c3107 --- /dev/null +++ b/tests/source/Overflows.scade @@ -0,0 +1,43 @@ +-- Root node: Top + +node BasicCount(reset : bool) returns (n : real) + n = CountToMax(reset, 3.0); + +node CountToMax(Reset : bool; Max : 'T) returns (N : 'T) where 'T numeric +var _L5 : 'T; +let + _L5 = fby (N; 8; (0: 'T)); + N = if Reset or Max < _L5 then (0: 'T) else (1: 'T) + _L5; +tel + +node CountToMaxNoReset(Max : 'T) returns (N : 'T) where 'T numeric +var _L5 : 'T; +let + _L5 = (0: 'T) -> pre N; + N = if Max < _L5 then (0: 'T) else (1: 'T) + _L5; +tel + +node Top(Input1 : int; Input2 : real; Input3 : bool) + returns (Output1 : int; + Output2 : real; + int_count, int_count1 : int; + real_count, real_count1 : real) +let + automaton SM1 + initial state State2 + unless + if Input3 restart State2; + var next : int; + let + next = if 100 < int_count1 then 0 else int_count1 + 1; + int_count1 = 0 -> pre next; + tel + + returns int_count1; + + real_count1 = (restart CountToMaxNoReset every Input3)(1000.); + int_count = CountToMax(Input3, 1000); + real_count = CountToMax(Input3, 1000.0); + Output2 = Input2 * 1.0e100; + Output1 = Input1 * 10000; +tel |