diff --git a/Cargo.lock b/Cargo.lock index 668b58c..0acbad6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -114,9 +114,9 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.5.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" [[package]] name = "backtrace" @@ -248,9 +248,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.20.2" +version = "3.20.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d20789868f4b01b2f2caec9f5c4e0213b41e3e5702a50157d699ae31ced2fcb" +checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" [[package]] name = "cactus" @@ -266,9 +266,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] name = "cc" -version = "1.2.60" +version = "1.2.62" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43c5703da9466b66a946814e1adf53ea2c90f10063b86290cc9eb67ce3478a20" +checksum = "a1dce859f0832a7d088c4f1119888ab94ef4b5d6795d1ce05afb7fe159d79f98" dependencies = [ "find-msvc-tools", "shlex", @@ -282,9 +282,9 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" [[package]] name = "cfgrammar" -version = "0.14.1" +version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3efdd8f0bddcc9e33f4a664d0f28bc4e51cd5367c16284087a95313104371865" +checksum = "b5ef80386dea3cda50570f22e1c6a474f0cc688ae220fc584fef354acaf41f2b" dependencies = [ "bincode", "indexmap", @@ -308,12 +308,12 @@ dependencies = [ [[package]] name = "chumsky" -version = "0.12.0" +version = "0.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ba4a05c9ce83b07de31b31c874e87c069881ac4355db9e752e3a55c11ec75a6" +checksum = "e0d2bfadce76f963d776feff99db6dc33783829539258314776383b33e2a00f8" dependencies = [ "hashbrown 0.15.5", - "regex-automata 0.3.9", + "regex-automata", "serde", "stacker", "unicode-ident", @@ -528,9 +528,9 @@ dependencies = [ [[package]] name = "displaydoc" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0" +checksum = "1ac70aa55017e108007fbaf5aa0f54b021c98f92ff8af59d42eda9da96e3dd4f" dependencies = [ "proc-macro2", "quote", @@ -539,9 +539,9 @@ dependencies = [ [[package]] name = "either" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" +checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e" [[package]] name = "encode_unicode" @@ -592,13 +592,12 @@ checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6" [[package]] name = "filetime" -version = "0.2.27" +version = "0.2.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f98844151eee8917efc50bd9e8318cb963ae8b297431495d3f758616ea5c57db" +checksum = "5c287a33c7f0a620c38e641e7f60827713987b3c0f26e8ddc9462cc69cf75759" dependencies = [ "cfg-if", "libc", - "libredox", ] [[package]] @@ -635,6 +634,30 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb" +[[package]] +name = "futures-core" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d" + +[[package]] +name = "futures-task" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393" + +[[package]] +name = "futures-util" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6" +dependencies = [ + "futures-core", + "futures-task", + "pin-project-lite", + "slab", +] + [[package]] name = "getopts" version = "0.2.24" @@ -705,9 +728,9 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.17.0" +version = "0.17.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f467dd6dccf739c208452f8014c75c18bb8301b050ad1cfb27153803edb0f51" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" [[package]] name = "heck" @@ -810,7 +833,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" dependencies = [ "equivalent", - "hashbrown 0.17.0", + "hashbrown 0.17.1", "serde", "serde_core", ] @@ -852,9 +875,9 @@ checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" [[package]] name = "jiff" -version = "0.2.23" +version = "0.2.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a3546dc96b6d42c5f24902af9e2538e82e39ad350b0c766eb3fbf2d8f3d8359" +checksum = "392c70591e8749fe235ddaf513e6f58b26bce3dcc16524cecc8936f75afa161e" dependencies = [ "jiff-static", "log", @@ -865,9 +888,9 @@ dependencies = [ [[package]] name = "jiff-static" -version = "0.2.23" +version = "0.2.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a8c8b344124222efd714b73bb41f8b5120b27a7cc1c75593a6ff768d9d05aa4" +checksum = "47b605b0c050d845fc355bb11eb3f9a8deddc218ea60c76e61aa1f2adfb2c96a" dependencies = [ "proc-macro2", "quote", @@ -876,10 +899,12 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.95" +version = "0.3.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2964e92d1d9dc3364cae4d718d93f227e3abb088e747d92e0395bfdedf1c12ca" +checksum = "142bc4740e452c1e57ade0cbc129f139c9093e354346f0872ef985f4f5cf5f11" dependencies = [ + "cfg-if", + "futures-util", "once_cell", "wasm-bindgen", ] @@ -892,21 +917,9 @@ checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" [[package]] name = "libc" -version = "0.2.185" +version = "0.2.186" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52ff2c0fe9bc6cb6b14a0592c2ff4fa9ceb83eea9db979b0487cd054946a2b8f" - -[[package]] -name = "libredox" -version = "0.1.16" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c" -dependencies = [ - "bitflags", - "libc", - "plain", - "redox_syscall", -] +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" [[package]] name = "litemap" @@ -916,9 +929,9 @@ checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0" [[package]] name = "log" -version = "0.4.29" +version = "0.4.30" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" +checksum = "616ec5685824bcc94416c6d4a7a446eea774a31efd7062c8480ba6fd06d7a6e5" [[package]] name = "logos" @@ -938,8 +951,8 @@ dependencies = [ "fnv", "proc-macro2", "quote", - "regex-automata 0.4.14", - "regex-syntax 0.8.10", + "regex-automata", + "regex-syntax", "syn", ] @@ -954,9 +967,9 @@ dependencies = [ [[package]] name = "lrlex" -version = "0.14.1" +version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eace1910351de39e720c0e765021cf9e3623fcb1a26943d7f4758da16c64e4f2" +checksum = "6faf26145c0571bcecf7887802d7dc2947154cb438801d6c90ef3633e68b2365" dependencies = [ "bincode", "cfgrammar", @@ -968,16 +981,16 @@ dependencies = [ "proc-macro2", "quote", "regex", - "regex-syntax 0.8.10", + "regex-syntax", "syn", "vergen", ] [[package]] name = "lrpar" -version = "0.14.1" +version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86be73e9299db43543922dbfd8faa3ae30c56f4ee9de18752ff1716001c71d91" +checksum = "402f799a7cfbaf548546e16191a15b7abaeb16ac25bbff5ab41fd93d7548d7a9" dependencies = [ "bincode", "cactus", @@ -1000,9 +1013,9 @@ dependencies = [ [[package]] name = "lrtable" -version = "0.14.1" +version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b15ad6a43e5cff4ac046d51281d2256a36d1440065eab53ccce9362b48db5b42" +checksum = "bcbe6a005a604615ab7aab7d1f74be563e508f5c6e42f85fbf65c38fe1f5f268" dependencies = [ "bincode", "cfgrammar", @@ -1014,9 +1027,9 @@ dependencies = [ [[package]] name = "memchr" -version = "2.8.0" +version = "2.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" +checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8" [[package]] name = "miniz_oxide" @@ -1049,9 +1062,9 @@ dependencies = [ [[package]] name = "num-conv" -version = "0.2.1" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c6673768db2d862beb9b39a78fdcb1a69439615d5794a1be50caa9bc92c81967" +checksum = "521739c6d2bac4aa25192232afe6841231376b2b26d4d9fae5ecf8ca5772e441" [[package]] name = "num-integer" @@ -1195,10 +1208,10 @@ dependencies = [ ] [[package]] -name = "plain" -version = "0.2.3" +name = "pin-project-lite" +version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" +checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" [[package]] name = "plotters" @@ -1289,9 +1302,9 @@ dependencies = [ [[package]] name = "quick-xml" -version = "0.39.2" +version = "0.40.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "958f21e8e7ceb5a1aa7fa87fab28e7c75976e0bfe7e23ff069e0a260f894067d" +checksum = "2474bd2e5029e7ccb6abb2ba48cf2383a333851dedf495901544281590c7da7f" dependencies = [ "memchr", ] @@ -1348,15 +1361,6 @@ dependencies = [ "crossbeam-utils", ] -[[package]] -name = "redox_syscall" -version = "0.7.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f450ad9c3b1da563fb6948a8e0fb0fb9269711c9c73d9ea1de5058c79c8d643a" -dependencies = [ - "bitflags", -] - [[package]] name = "regex" version = "1.12.3" @@ -1365,19 +1369,8 @@ checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.4.14", - "regex-syntax 0.8.10", -] - -[[package]] -name = "regex-automata" -version = "0.3.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59b23e92ee4318893fa3fe3e6fb365258efbfe6ac6ab30f090cdcbb7aa37efa9" -dependencies = [ - "aho-corasick", - "memchr", - "regex-syntax 0.7.5", + "regex-automata", + "regex-syntax", ] [[package]] @@ -1388,15 +1381,9 @@ checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.8.10", + "regex-syntax", ] -[[package]] -name = "regex-syntax" -version = "0.7.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da" - [[package]] name = "regex-syntax" version = "0.8.10" @@ -1490,9 +1477,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.149" +version = "1.0.150" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83fc039473c5595ace860d8c4fafa220ff474b3fc6bfdb4293327f1a37e94d86" +checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9" dependencies = [ "itoa", "memchr", @@ -1524,9 +1511,15 @@ checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214" [[package]] name = "siphasher" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2aa850e253778c88a04c3d7323b043aeda9d3e30d5971937c1855769763678e" +checksum = "8ee5873ec9cce0195efcb7a4e9507a04cd49aec9c83d0389df45b1ef7ba2e649" + +[[package]] +name = "slab" +version = "0.4.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" [[package]] name = "smallvec" @@ -1536,7 +1529,7 @@ checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" [[package]] name = "smc_scan" -version = "0.2.0" +version = "0.3.0" dependencies = [ "anyhow", "clap", @@ -1555,9 +1548,10 @@ dependencies = [ [[package]] name = "smc_scan_core" -version = "0.1.1" +version = "0.2.0" dependencies = [ "criterion", + "flate2", "log", "rand", "rayon", @@ -1567,22 +1561,36 @@ dependencies = [ [[package]] name = "smc_scan_jani" -version = "0.1.1" +version = "0.2.0" dependencies = [ "anyhow", "csv", "either", - "flate2", "log", "serde", "serde_json", "smc_scan_core", + "smc_scan_mtl", "thiserror", ] +[[package]] +name = "smc_scan_mtl" +version = "0.1.0" +dependencies = [ + "smc_scan_core", +] + +[[package]] +name = "smc_scan_pmtl" +version = "0.1.0" +dependencies = [ + "smc_scan_core", +] + [[package]] name = "smc_scan_promela" -version = "0.1.1" +version = "0.2.0" dependencies = [ "anyhow", "cfgrammar", @@ -1591,12 +1599,13 @@ dependencies = [ "lrpar", "regex", "smc_scan_core", + "smc_scan_pmtl", "thiserror", ] [[package]] name = "smc_scan_scxml" -version = "0.2.0" +version = "0.3.0" dependencies = [ "anyhow", "boa_ast", @@ -1604,11 +1613,11 @@ dependencies = [ "boa_parser", "chumsky", "csv", - "flate2", "log", "logos", "quick-xml", "smc_scan_core", + "smc_scan_pmtl", "thiserror", ] @@ -1906,9 +1915,9 @@ dependencies = [ [[package]] name = "wasm-bindgen" -version = "0.2.118" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0bf938a0bacb0469e83c1e148908bd7d5a6010354cf4fb73279b7447422e3a89" +checksum = "3ed04576f974d2b2fba0f38c51dbc5518011e38c36bf1143164be765528fd409" dependencies = [ "cfg-if", "once_cell", @@ -1919,9 +1928,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.118" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eeff24f84126c0ec2db7a449f0c2ec963c6a49efe0698c4242929da037ca28ed" +checksum = "916151b09da36bd82f6615cbf3a419e2f0ba23a03c6160e8e92eb6bd4aa1dec6" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1929,9 +1938,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.118" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9d08065faf983b2b80a79fd87d8254c409281cf7de75fc4b773019824196c904" +checksum = "299047362ccbfce148b67ab7e73349f77748e00c8296f9542adfad2ad82c5c5e" dependencies = [ "bumpalo", "proc-macro2", @@ -1942,9 +1951,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.118" +version = "0.2.122" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fd04d9e306f1907bd13c6361b5c6bfc7b3b3c095ed3f8a9246390f8dbdee129" +checksum = "9a929b2c61f11ba3e9bc35b50c1f25cb38e0e892c0c231ae2b8cf78d5dad4437" dependencies = [ "unicode-ident", ] @@ -1985,9 +1994,9 @@ dependencies = [ [[package]] name = "web-sys" -version = "0.3.95" +version = "0.3.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f2dfbb17949fa2088e5d39408c48368947b86f7834484e87b73de55bc14d97d" +checksum = "6d621441cfc37b84979402712047321980c178f299193a3589d05b99e8763436" dependencies = [ "js-sys", "wasm-bindgen", @@ -2278,18 +2287,18 @@ dependencies = [ [[package]] name = "zerocopy" -version = "0.8.48" +version = "0.8.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eed437bf9d6692032087e337407a86f04cd8d6a16a37199ed57949d415bd68e9" +checksum = "bce33a6288fa3f072a8c2c7d0f2fdbb90e28298f0135c1f99b96c3db2efcc60b" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.8.48" +version = "0.8.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70e3cd084b1788766f53af483dd21f93881ff30d7320490ec3ef7526d203bad4" +checksum = "8fd425244944f4ab65ccff928e7323354c5a018c75838362fdce749dfad2ee1e" dependencies = [ "proc-macro2", "quote", @@ -2298,9 +2307,9 @@ dependencies = [ [[package]] name = "zerofrom" -version = "0.1.7" +version = "0.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "69faa1f2a1ea75661980b013019ed6687ed0e83d069bc1114e2cc74c6c04c4df" +checksum = "0ec05a11813ea801ff6d75110ad09cd0824ddba17dfe17128ea0d5f68e6c5272" dependencies = [ "zerofrom-derive", ] diff --git a/Cargo.toml b/Cargo.toml index 922380a..98587f3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "smc_scan" -version = "0.2.1" +version = "0.3.0" edition = "2024" description = "Statistical model checker for large concurrent systems." documentation = "https://convince-project.github.io/scan/crates/scan/index.html" @@ -9,33 +9,41 @@ repository = "https://github.com/convince-project/scan" readme = "README.md" license = "Apache-2.0" keywords = ["verification", "model-checking"] -categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"] -exclude = [ - "scan_book/*", - ".github/*" +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" ] +exclude = ["scan_book/*", ".github/*"] [lib] -name = "scan" # The name of the target. -crate-type = ["lib"] # The crate types to generate. +name = "scan" # The name of the target. +crate-type = ["lib"] # The crate types to generate. [[bin]] -name = "scan" # The name of the target. +name = "scan" # The name of the target. path = "src/main.rs" [profile.release] lto = true codegen-units = 1 -# debug = true # only to run profiling # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [workspace] -members = ["scan_core", "scan_scxml", "scan_jani", "scan_promela"] +members = [ + "scan_core", + "scan_scxml", + "scan_jani", + "scan_promela", + "scan_pmtl", + "scan_mtl" +] [workspace.dependencies] anyhow = "1.0.102" csv = "1.4.0" -flate2 = { version = "1.1.9", features = ["zlib-rs"], default-features = false } log = "0.4.29" serde = { version = "1.0.228", features = ["derive"] } serde_json = "1.0.149" @@ -49,9 +57,9 @@ env_logger = "0.11.10" human-panic = "2.0.8" indicatif = { version = "0.18.4", features = ["improved_unicode"] } log = { workspace = true } -smc_scan_core = { version = "0.1.1", path = "scan_core" } -smc_scan_jani = { version = "0.1.1", path = "scan_jani" } -smc_scan_scxml = { version = "0.2.0", path = "scan_scxml" } -smc_scan_promela = { version = "0.1.1", path = "scan_promela" } +smc_scan_core = { version = "0.2.0", path = "scan_core" } +smc_scan_jani = { version = "0.2.0", path = "scan_jani" } +smc_scan_scxml = { version = "0.3.0", path = "scan_scxml" } +smc_scan_promela = { version = "0.2.0", path = "scan_promela" } serde = { workspace = true } serde_json = { workspace = true } diff --git a/scan_core/Cargo.toml b/scan_core/Cargo.toml index 83a8d2e..ef49c59 100644 --- a/scan_core/Cargo.toml +++ b/scan_core/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "smc_scan_core" -version = "0.1.1" +version = "0.2.0" edition = "2024" description = "Core module for the Scan model checker." documentation = "https://convince-project.github.io/scan/crates/scan_core/index.html" @@ -9,15 +9,22 @@ repository = "https://github.com/convince-project/scan" license = "Apache-2.0" readme = "README.md" keywords = ["verification", "model-checking"] -categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] [lib] -name = "scan_core" # The name of the target. -crate-type = ["lib"] # The crate types to generate. +name = "scan_core" # The name of the target. +crate-type = ["lib"] # The crate types to generate. [dependencies] thiserror = { workspace = true } log = { workspace = true } +flate2 = { version = "1.1.9", features = ["zlib-rs"], default-features = false } rand = { version = "0.10.1" } rayon = "1.12.0" smallvec = "1.15.1" diff --git a/scan_core/src/channel_system.rs b/scan_core/src/channel_system.rs index 5b16fe9..128e4b9 100644 --- a/scan_core/src/channel_system.rs +++ b/scan_core/src/channel_system.rs @@ -278,6 +278,15 @@ pub enum EventType { ProbeFullQueue, } +/// The capacity type of a channel: +#[derive(Debug, Clone, Copy)] +pub enum ChannelCapacity { + /// A (in)finite-capacity FIFO queue. + Queue(Option), + /// A channel that receives messages but never returns them. + Sink, +} + /// A definition object for a CS. /// It represents the abstract definition of a CS. /// @@ -314,7 +323,7 @@ pub enum EventType { /// ``` #[derive(Debug, Clone)] pub struct ChannelSystem { - channels: Vec<(Vec, Option)>, + channels: Vec<(Vec, ChannelCapacity)>, communications: Vec>, communications_pg_idxs: Vec, program_graphs: Vec, @@ -328,18 +337,24 @@ impl ChannelSystem { /// /// See also [`ProgramGraph::new_instance`]. pub fn new_instance<'def>(&'def self) -> ChannelSystemRun<'def> { + let pgs = self.program_graphs.len() as u16; + let mut pg_list = Vec::from_iter((0..pgs).map(PgId)); + pg_list.shrink_to_fit(); + ChannelSystemRun { rng: rand::make_rng(), time: 0, program_graphs: Vec::from_iter( self.program_graphs.iter().map(|pgdef| pgdef.new_instance()), ), - message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| { - cap.map_or_else(VecDeque::new, |cap| { + message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| match cap { + ChannelCapacity::Queue(queue) => queue.map_or_else(VecDeque::new, |cap| { VecDeque::with_capacity(types.len() * cap) - }) + }), + ChannelCapacity::Sink => VecDeque::new(), })), def: self, + pg_list, } } @@ -356,7 +371,7 @@ impl ChannelSystem { /// Returns the list of defined channels, given as the pair of their type and capacity /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity). #[inline] - pub fn channels(&self) -> &Vec<(Vec, Option)> { + pub fn channels(&self) -> &Vec<(Vec, ChannelCapacity)> { &self.channels } } @@ -374,6 +389,7 @@ pub struct ChannelSystemRun<'def> { message_queue: Vec>, program_graphs: Vec>, def: &'def ChannelSystem, + pg_list: Vec, } impl<'def> ChannelSystemRun<'def> { @@ -414,15 +430,23 @@ impl<'def> ChannelSystemRun<'def> { }) } - pub(crate) fn montecarlo_execution(&mut self) -> Option { - let pgs = self.program_graphs.len(); - let mut pg_vec = Vec::from_iter((0..pgs as u16).map(PgId)); + pub(crate) fn montecarlo_execution(&mut self) -> Option<(Action, Event)> { let mut rand1 = SmallRng::from_rng(&mut self.rng); let mut rand2 = SmallRng::from_rng(&mut self.rng); - while !pg_vec.is_empty() { - let pg_id = pg_vec.swap_remove(self.rng.random_range(0..pg_vec.len())); + // Setting pgs_left as length resets the queue + let mut pgs_left = self.pg_list.len(); + while pgs_left > 0 { + // Select random pg within 0..pgs_left + let pg_select = self.rng.random_range(0..pgs_left); + let pg_id = self.pg_list[pg_select]; + // Swap selected pg with last element of the queue (possibly itself, probably not worth checking) + // Decrease the length of the queue (so that selected element is removed) + pgs_left -= 1; + self.pg_list.swap(pg_select, pgs_left); // Execute randomly chosen transitions on the picked PG until an event is generated, // or no more transition is possible + // NOTE: Special treatment for PGs with single-location state for optimization of this common case. + // Hopefully it will be possible to treat all cases in a general way eventually. if self.program_graphs[pg_id.0 as usize].current_states().len() == 1 { while let Some((action, post_state)) = self.program_graphs[pg_id.0 as usize] .nosync_possible_transitions() @@ -442,7 +466,7 @@ impl<'def> ChannelSystemRun<'def> { .transition(pg_id, Action(pg_id, action), &[post_state]) .expect("successful transition"); if event.is_some() { - return event; + return event.map(|ev| (Action(pg_id, action), ev)); } } } else { @@ -465,7 +489,7 @@ impl<'def> ChannelSystemRun<'def> { .transition(pg_id, Action(pg_id, action), post_states.as_slice()) .expect("successful transition"); if event.is_some() { - return event; + return event.map(|ev| (Action(pg_id, action), ev)); } } } @@ -479,14 +503,20 @@ impl<'def> ChannelSystemRun<'def> { let (_, capacity) = self.def.channels[channel_idx]; let len = self.message_queue[channel_idx].len(); // Channel capacity must never be exceeded! - debug_assert!(capacity.is_none_or(|cap| len <= cap)); + // debug_assert!(capacity.is_none_or(|cap| len <= cap)); // NOTE FIXME currently handshake is unsupported // !matches!(capacity, Some(0)) - match message { - Message::Send => capacity.is_none_or(|cap| len < cap), - Message::Receive => len > 0, - Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap), - Message::ProbeEmptyQueue => len == 0, + match capacity { + ChannelCapacity::Queue(capacity) => match message { + Message::Send => capacity.is_none_or(|cap| len < cap), + Message::Receive => len > 0, + Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap), + Message::ProbeEmptyQueue => len == 0, + }, + ChannelCapacity::Sink => match message { + Message::Send | Message::ProbeEmptyQueue => true, + Message::Receive | Message::ProbeFullQueue => false, + }, } } @@ -499,25 +529,32 @@ impl<'def> ChannelSystemRun<'def> { let (_, capacity) = self.def.channels[channel.0 as usize]; let len = self.message_queue[channel.0 as usize].len(); // Channel capacity must never be exceeded! - assert!(capacity.is_none_or(|cap| len <= cap)); - match message { - Message::Send if capacity.is_some_and(|cap| len >= cap) => { - Err(CsError::OutOfCapacity(channel)) - } - Message::Receive if len == 0 => Err(CsError::Empty(channel)), - Message::ProbeEmptyQueue | Message::ProbeFullQueue - if matches!(capacity, Some(0)) => - { - Err(CsError::ProbingHandshakeChannel(channel)) - } - Message::ProbeFullQueue if capacity.is_none() => { - Err(CsError::ProbingInfiniteQueue(channel)) - } - Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)), - Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => { - Err(CsError::NotFull(channel)) - } - _ => Ok(()), + // assert!(capacity.is_none_or(|cap| len <= cap)); + match capacity { + ChannelCapacity::Queue(capacity) => match message { + Message::Send if capacity.is_some_and(|cap| len >= cap) => { + Err(CsError::OutOfCapacity(channel)) + } + Message::Receive if len == 0 => Err(CsError::Empty(channel)), + Message::ProbeEmptyQueue | Message::ProbeFullQueue + if matches!(capacity, Some(0)) => + { + Err(CsError::ProbingHandshakeChannel(channel)) + } + Message::ProbeFullQueue if capacity.is_none() => { + Err(CsError::ProbingInfiniteQueue(channel)) + } + Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)), + Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => { + Err(CsError::NotFull(channel)) + } + _ => Ok(()), + }, + ChannelCapacity::Sink => match message { + Message::Send | Message::ProbeEmptyQueue => Ok(()), + Message::ProbeFullQueue => Err(CsError::NotFull(channel)), + Message::Receive => Err(CsError::Empty(channel)), + }, } } else { Ok(()) @@ -548,8 +585,10 @@ impl<'def> ChannelSystemRun<'def> { let (_, capacity) = self.def.channels[channel.0 as usize]; let event_type = match message { Message::Send - if capacity - .is_some_and(|cap| self.message_queue[channel.0 as usize].len() >= cap) => + if let ChannelCapacity::Queue(capacity) = capacity + && capacity.is_some_and(|cap| { + self.message_queue[channel.0 as usize].len() >= cap + }) => { return Err(CsError::OutOfCapacity(channel)); } @@ -564,7 +603,9 @@ impl<'def> ChannelSystemRun<'def> { &mut self.rng, ) .map_err(|err| CsError::ProgramGraph(pg_id, err))?; - self.message_queue[channel.0 as usize].extend(vals.iter().copied()); + if matches!(capacity, ChannelCapacity::Queue(_)) { + self.message_queue[channel.0 as usize].extend(vals.iter().copied()); + } EventType::Send(vals) } Message::Receive if self.message_queue[channel.0 as usize].is_empty() => { @@ -588,7 +629,7 @@ impl<'def> ChannelSystemRun<'def> { EventType::Receive(vals) } Message::ProbeEmptyQueue | Message::ProbeFullQueue - if matches!(capacity, Some(0)) => + if matches!(capacity, ChannelCapacity::Queue(Some(0))) => { return Err(CsError::ProbingHandshakeChannel(channel)); } @@ -608,28 +649,29 @@ impl<'def> ChannelSystemRun<'def> { .map_err(|err| CsError::ProgramGraph(pg_id, err))?; EventType::ProbeEmptyQueue } - Message::ProbeFullQueue - if capacity - .is_some_and(|cap| self.message_queue[channel.0 as usize].len() < cap) => - { - return Err(CsError::NotFull(channel)); - } - Message::ProbeFullQueue if capacity.is_none() => { - return Err(CsError::ProbingInfiniteQueue(channel)); - } - Message::ProbeFullQueue => { - let _ = self.program_graphs[pg_id.0 as usize] - .send( - action.1, - post.iter() - .map(|loc| loc.1) - .collect::>() - .as_slice(), - &mut self.rng, - ) - .map_err(|err| CsError::ProgramGraph(pg_id, err))?; - EventType::ProbeFullQueue - } + Message::ProbeFullQueue => match capacity { + ChannelCapacity::Queue(None) => { + return Err(CsError::ProbingInfiniteQueue(channel)); + } + ChannelCapacity::Queue(Some(capacity)) => { + if self.message_queue[channel.0 as usize].len() >= capacity { + let _ = self.program_graphs[pg_id.0 as usize] + .send( + action.1, + post.iter() + .map(|loc| loc.1) + .collect::>() + .as_slice(), + &mut self.rng, + ) + .map_err(|err| CsError::ProgramGraph(pg_id, err))?; + EventType::ProbeFullQueue + } else { + return Err(CsError::NotFull(channel)); + } + } + ChannelCapacity::Sink => return Err(CsError::NotFull(channel)), + }, }; Ok(Some(Event { pg_id, diff --git a/scan_core/src/channel_system/builder.rs b/scan_core/src/channel_system/builder.rs index 3b0b680..644f7d4 100644 --- a/scan_core/src/channel_system/builder.rs +++ b/scan_core/src/channel_system/builder.rs @@ -2,6 +2,7 @@ use super::{ Action, Channel, ChannelSystem, Clock, CsError, Location, Message, PgError, PgExpression, PgId, ProgramGraphBuilder, TimeConstraint, Var, }; +use crate::channel_system::ChannelCapacity; use crate::grammar::{BooleanExpr, Type}; use crate::program_graph::ProgramGraph; use crate::{Expression, Val}; @@ -28,7 +29,7 @@ impl From<(PgId, CsExpression)> for PgExpression { /// The object used to define and build a CS. pub struct ChannelSystemBuilder { program_graphs: Vec, - channels: Vec<(Vec, Option)>, + channels: Vec<(Vec, ChannelCapacity)>, communications: BTreeMap>, } @@ -464,7 +465,15 @@ impl ChannelSystemBuilder { /// - [`Some(0)`] capacity means the channel uses the handshake protocol (NOT YET IMPLEMENTED!) pub fn new_channel(&mut self, var_types: Vec, capacity: Option) -> Channel { let channel = Channel(self.channels.len() as u16); - self.channels.push((var_types, capacity)); + self.channels + .push((var_types, ChannelCapacity::Queue(capacity))); + channel + } + + /// Adds a new sink of the given type to the CS. + pub fn new_sink(&mut self, var_types: Vec) -> Channel { + let channel = Channel(self.channels.len() as u16); + self.channels.push((var_types, ChannelCapacity::Sink)); channel } @@ -555,7 +564,7 @@ impl ChannelSystemBuilder { .channels .get(channel.0 as usize) .ok_or(CsError::MissingChannel(channel))?; - if matches!(cap, Some(0)) { + if matches!(cap, ChannelCapacity::Queue(Some(0))) { // it makes no sense to probe an handshake channel Err(CsError::ProbingHandshakeChannel(channel)) } else { @@ -585,10 +594,10 @@ impl ChannelSystemBuilder { .channels .get(channel.0 as usize) .ok_or(CsError::MissingChannel(channel))?; - if matches!(cap, Some(0)) { + if matches!(cap, ChannelCapacity::Queue(Some(0))) { // it makes no sense to probe an handshake channel Err(CsError::ProbingHandshakeChannel(channel)) - } else if cap.is_none() { + } else if matches!(cap, ChannelCapacity::Queue(None)) { // it makes no sense to probe for fullness an handshake channel Err(CsError::ProbingInfiniteQueue(channel)) } else { diff --git a/scan_core/src/cs_model.rs b/scan_core/src/cs_model.rs deleted file mode 100644 index 16c2cd5..0000000 --- a/scan_core/src/cs_model.rs +++ /dev/null @@ -1,148 +0,0 @@ -use crate::TransitionSystemGenerator; -use crate::channel_system::{ - Channel, ChannelSystem, ChannelSystemBuilder, ChannelSystemRun, Event, EventType, -}; -use crate::{DummyRng, Expression, Time, Val, transition_system::TransitionSystem}; - -/// An atomic variable for [`crate::Pmtl`] formulae. -#[derive(Debug, Clone)] -pub enum Atom { - /// A predicate. - State(Channel, usize), - /// An event. - Event(Event), -} - -/// A definition type that instances new [`CsModelRun`]. -#[derive(Debug, Clone)] -pub struct CsModel { - cs: ChannelSystem, - ports: Vec>>, - predicates: Vec>, -} - -impl CsModel { - /// Creates a new [`CsModel`] from a [`ChannelSystemBuilder`]. - pub fn new(cs: ChannelSystemBuilder) -> Self { - // TODO: Check predicates are Boolean expressions and that conversion does not fail - let cs = cs.build(); - Self { - ports: cs - .channels() - .iter() - .map(|(types, _)| vec![None; types.len()]) - .collect(), - cs, - predicates: Vec::new(), - } - } - - /// Adds a new port to the [`CsModel`], - /// which is given by an [`Channel`] and a default [`Val`] value. - pub fn add_port(&mut self, channel: Channel, idx: usize, default: Val) { - // TODO FIXME: error handling and type checking. - self.ports[u16::from(channel) as usize][idx] = Some(default); - } - - /// Adds a new predicate to the [`CsModel`], - /// which is an expression over the CS's channels. - pub fn add_predicate(&mut self, predicate: Expression) -> usize { - let _ = predicate.eval( - &|port| match port { - Atom::State(channel, idx) => self.ports[u16::from(*channel) as usize][*idx] - .expect("port must have been initialized"), - Atom::Event(_event) => Val::Boolean(false), - }, - &mut DummyRng, - ); - self.predicates.push(predicate); - self.predicates.len() - 1 - } -} - -impl TransitionSystemGenerator for CsModel { - type Ts<'a> - = CsModelRun<'a> - where - Self: 'a; - - fn generate<'a>(&'a self) -> Self::Ts<'a> { - CsModelRun { - cs: self.cs.new_instance(), - ports: self.ports.clone(), - predicates: &self.predicates, - last_event: None, - } - } -} - -/// Transition system model based on a [`ChannelSystem`]. -/// -/// It is essentially a CS which keeps track of the [`Event`]s produced by the execution -/// and determining a set of predicates. -#[derive(Debug, Clone)] -pub struct CsModelRun<'def> { - cs: ChannelSystemRun<'def>, - ports: Vec>>, - // TODO: predicates should not use rng - predicates: &'def [Expression], - last_event: Option, -} - -impl<'def> TransitionSystem for CsModelRun<'def> { - type Event = Event; - - fn transition(&mut self) -> Option { - let event = self.cs.montecarlo_execution(); - if let Some(ref event) = event - && let EventType::Send(ref vals) = event.event_type - { - let port = self - .ports - .get_mut(u16::from(event.channel) as usize) - .expect("port must exist"); - port.iter_mut().zip(vals).for_each(|(p, &v)| { - if p.is_some() { - *p = Some(v) - } - }); - } - self.last_event = event.clone(); - event - } - - #[inline] - fn time(&self) -> Time { - self.cs.time() - } - - #[inline] - fn time_tick(&mut self) { - self.cs.wait(1).expect("time error") - } - - fn labels(&self) -> impl Iterator { - self.predicates.iter().map(|prop| { - if let Val::Boolean(b) = prop.eval( - &|port| match port { - Atom::State(channel, idx) => self.ports[u16::from(*channel) as usize][*idx] - .expect("port must exist and be initialized"), - Atom::Event(event) => { - Val::Boolean(self.last_event.as_ref().is_some_and(|e| e == event)) - } - }, - &mut DummyRng, - ) { - b - } else { - // FIXME: handle error or guarantee it won't happen - panic!("propositions should evaluate to boolean values") - } - }) - } - - #[inline] - fn state(&self) -> impl Iterator { - self.ports.iter().flat_map(|p| p.iter().filter_map(|p| *p)) - } -} diff --git a/scan_core/src/dummy_rng.rs b/scan_core/src/dummy_rng.rs deleted file mode 100644 index 32cbca4..0000000 --- a/scan_core/src/dummy_rng.rs +++ /dev/null @@ -1,30 +0,0 @@ -use rand::SeedableRng; -use rand::rand_core::TryRng; - -#[derive(Debug, Clone)] -pub(crate) struct DummyRng; - -impl TryRng for DummyRng { - type Error = core::convert::Infallible; - - fn try_next_u32(&mut self) -> Result { - panic!("DummyRng should never be called") - } - - fn try_next_u64(&mut self) -> Result { - panic!("DummyRng should never be called") - } - - fn try_fill_bytes(&mut self, dst: &mut [u8]) -> Result<(), Self::Error> { - let _ = dst; - panic!("DummyRng should never be called") - } -} - -impl SeedableRng for DummyRng { - type Seed = [u8; 0]; - - fn from_seed(_seed: Self::Seed) -> Self { - Self - } -} diff --git a/scan_core/src/grammar.rs b/scan_core/src/grammar.rs index 1e4c544..64bf2ac 100644 --- a/scan_core/src/grammar.rs +++ b/scan_core/src/grammar.rs @@ -10,15 +10,13 @@ mod float; mod integer; mod natural; -use rand::Rng; +use rand::{Rng, rngs::SmallRng}; use std::{ hash::Hash, ops::{Add, BitAnd, BitOr, Div, Mul, Neg, Not, Rem}, }; use thiserror::Error; -use crate::dummy_rng::DummyRng; - pub use boolean::*; pub use float::*; pub use integer::*; @@ -34,9 +32,6 @@ pub enum TypeError { /// The variable's type is unknown. #[error("the type of variable is unknown")] UnknownVar, - /// Bounds violate some constraint. - #[error("the bounds violate some constraint")] - BadBounds, /// Probability violates some constraint. #[error("the probability violates some constraint")] BadProbability, @@ -187,9 +182,18 @@ where } } +impl From<(V, Type)> for Expression +where + V: Copy, +{ + fn from((var, r#type): (V, Type)) -> Self { + Expression::from_var(var, r#type) + } +} + impl Expression where - V: Clone, + V: Copy, { /// Computes the type of an expression. /// @@ -208,7 +212,7 @@ where /// /// Will assume the expression (with the variable assignment) is well-typed, /// and may panic if producing an unexpected type. - pub fn eval(&self, vars: &dyn Fn(&V) -> Val, rng: &mut R) -> Val { + pub fn eval(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option) -> Val { match self { Expression::Boolean(boolean_expr) => Val::Boolean(boolean_expr.eval(vars, rng)), Expression::Natural(natural_expr) => Val::Natural(natural_expr.eval(vars, rng)), @@ -217,6 +221,27 @@ where } } + /// Evaluates the expression with the given variable assignments. + /// + /// Will assume the expression (with the variable assignment) is well-typed, + /// and may panic if producing an unexpected type. + pub fn eval_deterministic(&self, vars: &dyn Fn(V) -> Val) -> Val { + match self { + Expression::Boolean(boolean_expr) => { + Val::Boolean(boolean_expr.eval::(vars, &mut None)) + } + Expression::Natural(natural_expr) => { + Val::Natural(natural_expr.eval::(vars, &mut None)) + } + Expression::Integer(integer_expr) => { + Val::Integer(integer_expr.eval::(vars, &mut None)) + } + Expression::Float(float_expr) => { + Val::Float(float_expr.eval::(vars, &mut None)) + } + } + } + /// Evals a constant expression. /// Returns an error if expression contains variables. pub fn is_constant(&self) -> bool { @@ -232,7 +257,7 @@ where /// Returns an error if expression contains variables. pub fn eval_constant(&self) -> Result { if self.is_constant() { - Ok(self.eval(&|_| panic!("no vars"), &mut DummyRng)) + Ok(self.eval::(&|_| panic!("no vars"), &mut None)) } else { Err(TypeError::UnknownVar) } diff --git a/scan_core/src/grammar/boolean.rs b/scan_core/src/grammar/boolean.rs index 023db60..ab5c28f 100644 --- a/scan_core/src/grammar/boolean.rs +++ b/scan_core/src/grammar/boolean.rs @@ -74,7 +74,7 @@ where impl BooleanExpr where - V: Clone, + V: Copy, { /// Returns `true` if the expression is constant, i.e., it contains no variables, and `false` otherwise. pub fn is_constant(&self) -> bool { @@ -124,11 +124,11 @@ where /// /// - If a variable is not included in the evaluation; /// - If a variable included in the evaluation is not of Boolean type. - pub fn eval(&self, vars: &dyn Fn(&V) -> Val, rng: &mut R) -> bool { + pub fn eval(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option) -> bool { match self { BooleanExpr::Const(b) => *b, BooleanExpr::Var(var) => { - if let Val::Boolean(b) = vars(var) { + if let Val::Boolean(b) = vars(*var) { b } else { panic!("type mismatch: expected boolean variable") @@ -136,7 +136,7 @@ where } BooleanExpr::Rand(float_expr) => { let bernoulli = float_expr.eval(vars, rng); - rng.random_bool(bernoulli) + rng.as_mut().expect("rng").random_bool(bernoulli) } BooleanExpr::And(boolean_exprs) => boolean_exprs .iter() @@ -282,7 +282,7 @@ where pub(crate) fn context(&self, vars: &dyn Fn(V) -> Option) -> Result<(), TypeError> { match self { BooleanExpr::Const(_) => Ok(()), - BooleanExpr::Var(v) => matches!(vars(v.clone()), Some(Type::Boolean)) + BooleanExpr::Var(v) => matches!(vars(*v), Some(Type::Boolean)) .then_some(()) .ok_or(TypeError::TypeMismatch), BooleanExpr::Rand(float_expr) => float_expr.context(vars), diff --git a/scan_core/src/grammar/float.rs b/scan_core/src/grammar/float.rs index 45e63d0..4bc9d0d 100644 --- a/scan_core/src/grammar/float.rs +++ b/scan_core/src/grammar/float.rs @@ -54,7 +54,7 @@ where impl FloatExpr where - V: Clone, + V: Copy, { /// Returns `true` if the expression is constant, i.e., it contains no variables, and `false` otherwise. pub fn is_constant(&self) -> bool { @@ -87,11 +87,11 @@ where /// - If a variable included in the evaluation is not of [`Float`] type; /// - Division by 0; /// - Overflow. - pub fn eval(&self, vars: &dyn Fn(&V) -> Val, rng: &mut R) -> Float { + pub fn eval(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option) -> Float { match self { FloatExpr::Const(float) => *float, FloatExpr::Var(var) => { - if let Val::Float(float) = vars(var) { + if let Val::Float(float) = vars(*var) { float } else { panic!("type mismatch: expected float variable") @@ -105,7 +105,9 @@ where let (lower_bound_expr, upper_bound_expr) = bounds.as_ref(); let lower_bound = lower_bound_expr.eval(vars, rng); let upper_bound = upper_bound_expr.eval(vars, rng); - rng.random_range(lower_bound..upper_bound) + rng.as_mut() + .expect("rng") + .random_range(lower_bound..upper_bound) } FloatExpr::Opposite(float_expr) => -float_expr.eval(vars, rng), FloatExpr::Sum(float_exprs) => { @@ -163,7 +165,7 @@ where pub(crate) fn context(&self, vars: &dyn Fn(V) -> Option) -> Result<(), TypeError> { match self { FloatExpr::Const(_) => Ok(()), - FloatExpr::Var(v) => matches!(vars(v.clone()), Some(Type::Float)) + FloatExpr::Var(v) => matches!(vars(*v), Some(Type::Float)) .then_some(()) .ok_or(TypeError::TypeMismatch), FloatExpr::Nat(natural_expr) => natural_expr.context(vars), diff --git a/scan_core/src/grammar/integer.rs b/scan_core/src/grammar/integer.rs index b41ab51..52b79a6 100644 --- a/scan_core/src/grammar/integer.rs +++ b/scan_core/src/grammar/integer.rs @@ -45,6 +45,8 @@ where Rem(Box<(IntegerExpr, IntegerExpr)>), /// Floor Floor(Box>), + /// Ceil + Ceil(Box>), // ----- // Flow // ----- @@ -56,7 +58,7 @@ where impl IntegerExpr where - V: Clone, + V: Copy, { /// Returns `true` if the expression is constant, i.e., it contains no variables, and `false` otherwise. pub fn is_constant(&self) -> bool { @@ -72,7 +74,9 @@ where let (lhs, rhs) = args.as_ref(); lhs.is_constant() && rhs.is_constant() } - IntegerExpr::Floor(float_expr) => float_expr.is_constant(), + IntegerExpr::Floor(float_expr) | IntegerExpr::Ceil(float_expr) => { + float_expr.is_constant() + } IntegerExpr::Ite(args) => { let (ite, lhs, rhs) = args.as_ref(); ite.is_constant() && lhs.is_constant() && rhs.is_constant() @@ -88,11 +92,11 @@ where /// - If a variable included in the evaluation is not of [`Integer`] type; /// - Division by 0; /// - Overflow. - pub fn eval(&self, vars: &dyn Fn(&V) -> Val, rng: &mut R) -> Integer { + pub fn eval(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option) -> Integer { match self { IntegerExpr::Const(int) => *int, IntegerExpr::Var(var) => { - if let Val::Integer(int) = vars(var) { + if let Val::Integer(int) = vars(*var) { int } else { panic!("type mismatch: expected natural variable") @@ -103,7 +107,9 @@ where let (lower_bound_expr, upper_bound_expr) = bounds.as_ref(); let lower_bound = lower_bound_expr.eval(vars, rng); let upper_bound = upper_bound_expr.eval(vars, rng); - rng.random_range(lower_bound..upper_bound) + rng.as_mut() + .expect("rng") + .random_range(lower_bound..upper_bound) } IntegerExpr::Opposite(integer_expr) => integer_expr.eval(vars, rng).strict_neg(), IntegerExpr::Sum(integer_exprs) => integer_exprs @@ -124,8 +130,8 @@ where let rhs = rhs_expr.eval(vars, rng); lhs.strict_rem_euclid(rhs) } - // NOTE WARN: is float-to-int floor operation sound? IntegerExpr::Floor(float_expr) => float_expr.eval(vars, rng).floor() as Integer, + IntegerExpr::Ceil(float_expr) => float_expr.eval(vars, rng).ceil() as Integer, IntegerExpr::Ite(args) => { let (ite, lhs, rhs) = args.as_ref(); if ite.eval(vars, rng) { @@ -170,6 +176,7 @@ where IntegerExpr::Rem(Box::new((lhs.map(map), rhs.map(map)))) } IntegerExpr::Floor(float_expr) => IntegerExpr::Floor(Box::new(float_expr.map(map))), + IntegerExpr::Ceil(float_expr) => IntegerExpr::Ceil(Box::new(float_expr.map(map))), IntegerExpr::Ite(args) => { let (r#if, then, r#else) = *args; IntegerExpr::Ite(Box::new((r#if.map(map), then.map(map), r#else.map(map)))) @@ -180,7 +187,7 @@ where pub(crate) fn context(&self, vars: &dyn Fn(V) -> Option) -> Result<(), TypeError> { match self { IntegerExpr::Const(_) => Ok(()), - IntegerExpr::Var(v) => matches!(vars(v.clone()), Some(Type::Integer)) + IntegerExpr::Var(v) => matches!(vars(*v), Some(Type::Integer)) .then_some(()) .ok_or(TypeError::TypeMismatch), IntegerExpr::Nat(natural_expr) => natural_expr.context(vars), @@ -191,7 +198,9 @@ where IntegerExpr::Sum(integer_exprs) | IntegerExpr::Product(integer_exprs) => { integer_exprs.iter().try_for_each(|expr| expr.context(vars)) } - IntegerExpr::Floor(float_expr) => float_expr.context(vars), + IntegerExpr::Floor(float_expr) | IntegerExpr::Ceil(float_expr) => { + float_expr.context(vars) + } IntegerExpr::Ite(exprs) => exprs .0 .context(vars) diff --git a/scan_core/src/grammar/natural.rs b/scan_core/src/grammar/natural.rs index b61fda9..52ef928 100644 --- a/scan_core/src/grammar/natural.rs +++ b/scan_core/src/grammar/natural.rs @@ -52,7 +52,7 @@ where impl NaturalExpr where - V: Clone, + V: Copy, { /// Returns `true` if the expression is constant, i.e., it contains no variables, and `false` otherwise. pub fn is_constant(&self) -> bool { @@ -82,11 +82,11 @@ where /// - If a variable included in the evaluation is not of [`Natural`] type; /// - Division by 0; /// - Overflow. - pub fn eval(&self, vars: &dyn Fn(&V) -> Val, rng: &mut R) -> Natural { + pub fn eval(&self, vars: &dyn Fn(V) -> Val, rng: &mut Option) -> Natural { match self { NaturalExpr::Const(nat) => *nat, NaturalExpr::Var(var) => { - if let Val::Natural(nat) = vars(var) { + if let Val::Natural(nat) = vars(*var) { nat } else { panic!("type mismatch: expected natural variable") @@ -96,7 +96,9 @@ where let (lower_bound_expr, upper_bound_expr) = bounds.as_ref(); let lower_bound = lower_bound_expr.eval(vars, rng); let upper_bound = upper_bound_expr.eval(vars, rng); - rng.random_range(lower_bound..upper_bound) + rng.as_mut() + .expect("rng") + .random_range(lower_bound..upper_bound) } NaturalExpr::Sum(natural_exprs) => natural_exprs .iter() @@ -162,7 +164,7 @@ where pub(crate) fn context(&self, vars: &dyn Fn(V) -> Option) -> Result<(), TypeError> { match self { NaturalExpr::Const(_) => Ok(()), - NaturalExpr::Var(v) => matches!(vars(v.clone()), Some(Type::Natural)) + NaturalExpr::Var(v) => matches!(vars(*v), Some(Type::Natural)) .then_some(()) .ok_or(TypeError::TypeMismatch), NaturalExpr::Rand(exprs) | NaturalExpr::Div(exprs) | NaturalExpr::Rem(exprs) => { diff --git a/scan_core/src/lib.rs b/scan_core/src/lib.rs index 58475f8..3120a85 100644 --- a/scan_core/src/lib.rs +++ b/scan_core/src/lib.rs @@ -7,32 +7,33 @@ #![forbid(unsafe_code)] pub mod channel_system; -mod cs_model; -mod dummy_rng; mod grammar; mod oracle; -mod pg_model; pub mod program_graph; mod smc; +mod tracer; mod transition_system; -use core::marker::Sync; -pub use cs_model::{Atom, CsModel, CsModelRun}; -use dummy_rng::DummyRng; pub use grammar::*; use log::{info, trace}; pub use oracle::*; -pub use pg_model::{PgModel, PgModelRun}; use rayon::iter::{IntoParallelIterator, ParallelIterator}; pub use smc::*; use std::{ + fs::{File, create_dir, create_dir_all, rename}, + path::PathBuf, sync::{ Arc, Mutex, atomic::{AtomicBool, AtomicU32, Ordering}, }, time::Instant, }; -pub use transition_system::{Tracer, TransitionSystem, TransitionSystemGenerator}; +pub use tracer::{TraceWriter, Tracer}; +pub use transition_system::{Atom, TransitionSystem, TransitionSystemRun}; + +const TEMP: &str = ".temp"; +const SUCCESSES: &str = "successes"; +const FAILURES: &str = "failures"; /// The type that represents time. pub type Time = u32; @@ -48,11 +49,11 @@ pub enum RunOutcome { /// The main type to interface with the verification capabilities of SCAN. /// [`Scan`] holds the model, properties and other data necessary to run the verification process. -/// The type of models and properties is abstracted through the [`TransitionSystem`] and [`Oracle`] traits, +/// The type of models and properties is abstracted through the [`Oracle`] trait, /// to provide a unified interface. #[derive(Debug, Clone)] -pub struct Scan { - tsd: TsG, +pub struct Scan { + model: TransitionSystem, oracle: O, running: Arc, successes: Arc, @@ -60,11 +61,11 @@ pub struct Scan { violations: Arc>>, } -impl Scan { +impl Scan { /// Create new [`Scan`] object. - pub fn new(tsd: TsG, oracle: O) -> Self { + pub fn new(tsd: TransitionSystem, oracle: O) -> Self { Scan { - tsd, + model: tsd, oracle, running: Arc::new(AtomicBool::new(false)), successes: Arc::new(AtomicU32::new(0)), @@ -105,13 +106,15 @@ impl Scan { } } -impl Scan { +impl Scan { fn verification(&self, confidence: f64, precision: f64, duration: Time) { let local_successes; let local_failures; - let mut ts = self.tsd.generate(); - let result = ts.experiment(duration, self.oracle.clone(), self.running.clone()); + let result = + self.model + .new_run() + .experiment(duration, self.oracle.clone(), self.running.clone()); if !self.running.load(Ordering::Relaxed) { return; } @@ -171,40 +174,66 @@ impl Scan { .count(); let elapsed = start_time.elapsed(); - info!("verification time elapsed: {elapsed:0.2?}"); - info!("verification terminating"); - } - - #[inline] - fn trace<'a, T>(&'a self, tracer: T, duration: Time) - where - T: Tracer<<::Ts<'a> as TransitionSystem>::Event>, - { - let mut ts = self.tsd.generate(); - ts.trace(duration, self.oracle.clone(), tracer) + info!("verification completed in {elapsed:0.2?}"); } /// Produces and saves the traces for the given number of runs, /// using the provided [`Tracer`]. - pub fn traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time) + pub fn traces(&self, runs: usize, duration: Time, path: PathBuf, model_data: &T::ModelData) where - T: Clone + Tracer<<::Ts<'a> as TransitionSystem>::Event>, + T: Tracer, { // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al. info!("tracing starting"); let start_time = Instant::now(); + create_traces_dirs_tree(path.clone()); - (0..runs).for_each(|_| self.trace::(tracer.clone(), duration)); + (0..runs).for_each(|idx| { + self.trace::(duration, path.clone(), model_data, idx); + }); let elapsed = start_time.elapsed(); - info!("tracing time elapsed: {elapsed:0.2?}"); - info!("tracing terminating"); + info!("tracing completed in {elapsed:0.2?}"); + } + + fn trace(&self, duration: u32, mut path: PathBuf, model_data: &T::ModelData, idx: usize) + where + T: Tracer, + { + let mut ts = self.model.new_run(); + let filename = PathBuf::new() + .with_file_name(format!("{idx:04}")) + .with_extension(T::EXTENSION); + path.push(crate::TEMP); + path.push(&filename); + path.add_extension("gz"); + let file = File::create_new(&path).expect("create file"); + let writer = flate2::GzBuilder::new() + .filename(filename.to_str().expect("file name")) + .comment("Scan-generated execution trace") + .write(file, flate2::Compression::best()); + let tracer = T::init(writer, model_data); + if let RunOutcome::Verified(verified) = + ts.trace::(duration, self.oracle.clone(), tracer, model_data) + { + let mut new_path = path.clone(); + // pop file name + new_path.pop(); + // pop temp folder + new_path.pop(); + if verified.iter().all(|b| *b) { + new_path.push(crate::SUCCESSES); + } else { + new_path.push(crate::FAILURES); + } + new_path.push(path.file_name().expect("file name")); + rename(&path, new_path).expect("renaming"); + } } } -impl Scan +impl Scan where - TsG: TransitionSystemGenerator + Sync, O: Oracle + Sync, { /// Statistically verifies the provided [`TransitionSystem`] using adaptive bound and the given parameters, @@ -226,29 +255,44 @@ where .count(); let elapsed = start_time.elapsed(); - info!("verification time elapsed: {elapsed:0.2?}"); - info!("verification terminating"); + info!("verification completed in {elapsed:0.2?}"); } /// Produces and saves the traces for the given number of runs, /// using the provided [`Tracer`], /// spawning multiple threads. - pub fn par_traces<'a, T>(&'a self, runs: usize, tracer: T, duration: Time) - where - T: Clone - + Sync - + Tracer<<::Ts<'a> as TransitionSystem>::Event>, + pub fn par_traces( + &self, + runs: usize, + duration: Time, + path: PathBuf, + model_data: &T::ModelData, + ) where + T: Tracer, + T::ModelData: Sync, { // WARN FIXME TODO: Implement algorithm for 2.4 Distributed sample generation in Budde et al. info!("tracing starting"); let start_time = Instant::now(); + create_traces_dirs_tree(path.clone()); - (0..runs) - .into_par_iter() - .for_each(|_| self.trace::(tracer.clone(), duration)); + (0..runs).into_par_iter().for_each(|idx| { + self.trace::(duration, path.clone(), model_data, idx); + }); let elapsed = start_time.elapsed(); - info!("tracing time elapsed: {elapsed:0.2?}"); - info!("tracing terminating"); + info!("tracing completed in {elapsed:0.2?}"); } } + +fn create_traces_dirs_tree(mut path: PathBuf) { + create_dir_all(&path).expect("create base dir"); + path.push(TEMP); + create_dir(&path).expect("create temp dir"); + assert!(path.pop()); + path.push(SUCCESSES); + create_dir(&path).expect("create successes dir"); + assert!(path.pop()); + path.push(FAILURES); + create_dir(&path).expect("create failures dir"); +} diff --git a/scan_core/src/oracle.rs b/scan_core/src/oracle.rs index 0483dae..08899b0 100644 --- a/scan_core/src/oracle.rs +++ b/scan_core/src/oracle.rs @@ -1,9 +1,4 @@ -mod mtl; -mod pmtl; - use crate::Time; -pub use mtl::{Mtl, MtlOracle}; -pub use pmtl::{Pmtl, PmtlOracle}; /// Implementators are induced by a temporal property. /// They can update their internal state when fed a new state of a trace, diff --git a/scan_core/src/pg_model.rs b/scan_core/src/pg_model.rs deleted file mode 100644 index ea5245e..0000000 --- a/scan_core/src/pg_model.rs +++ /dev/null @@ -1,94 +0,0 @@ -use rand::rngs::SmallRng; - -use crate::{ - Expression, Time, TransitionSystem, Val, - program_graph::{ - Action, PgExpression, ProgramGraph, ProgramGraphBuilder, ProgramGraphRun, Var, - }, - transition_system::TransitionSystemGenerator, -}; - -/// A [`ProgramGraph`]-based model implementing [`TransitionSystem`] with synchronous concurrency. -#[derive(Debug, Clone)] -pub struct PgModel { - pg: ProgramGraph, - global_vars: Vec, - predicates: Vec>, -} - -impl PgModel { - /// Create a new [`PgModel`] from the given [`ProgramGraph`] and predicates over its internal state. - pub fn new( - pg: ProgramGraphBuilder, - global_vars: Vec, - predicates: Vec, - ) -> Self { - let pg = pg.build(); - Self { - pg, - global_vars, - predicates, - } - } -} - -impl TransitionSystemGenerator for PgModel { - type Ts<'a> - = PgModelRun<'a> - where - Self: 'a; - - fn generate<'a>(&'a self) -> Self::Ts<'a> { - PgModelRun { - pg: self.pg.new_instance(), - rng: rand::make_rng(), - global_vars: &self.global_vars, - predicates: &self.predicates, - time: 0, - } - } -} - -/// A model based on a single [`ProgramGraph`], -/// with predicates over the PG's variables. -#[derive(Debug, Clone)] -pub struct PgModelRun<'def> { - pg: ProgramGraphRun<'def>, - rng: SmallRng, - global_vars: &'def [Var], - predicates: &'def [Expression], - time: Time, -} - -impl<'def> TransitionSystem for PgModelRun<'def> { - type Event = Action; - - fn transition(&mut self) -> Option { - self.pg.montecarlo(&mut self.rng) - } - - fn time(&self) -> Time { - self.time - } - - fn time_tick(&mut self) { - self.time += 1; - } - - fn labels(&self) -> impl Iterator { - self.predicates.iter().map(|p| { - if let Val::Boolean(b) = self.pg.eval(p) { - b - } else { - panic!("non-bool pred") - } - }) - } - - fn state(&self) -> impl Iterator { - self.global_vars - .as_ref() - .iter() - .map(|var| self.pg.val(*var).expect("value")) - } -} diff --git a/scan_core/src/program_graph.rs b/scan_core/src/program_graph.rs index 22dc1ff..33d278f 100644 --- a/scan_core/src/program_graph.rs +++ b/scan_core/src/program_graph.rs @@ -79,9 +79,9 @@ mod builder; -use crate::{DummyRng, Time, grammar::*}; +use crate::{Time, grammar::*}; pub use builder::*; -use rand::{Rng, SeedableRng, seq::IteratorRandom}; +use rand::{Rng, rngs::SmallRng}; use smallvec::SmallVec; use thiserror::Error; @@ -292,6 +292,54 @@ impl ProgramGraph { } } +// WARN: This iterator allocates a [`Vec`] every time `next` is called. +// To avoid this, one way would be to allocate a vector at creation and return a reference to it +// for every iteration of next, but this requires "streaming iterators" or analogous solution. +// TODO: Find a way to implement preallocation (or no allocation). +struct TransitionsIterator<'a, I: Iterator> { + iters: Vec, + // vals: Vec<&'a [Transition]>, +} + +impl<'a, I: Iterator> TransitionsIterator<'a, I> { + fn new(iters: Vec) -> Self { + Self { + // vals: Vec::with_capacity(iters.len()), + iters, + } + } +} + +impl<'a, I: Iterator> Iterator for TransitionsIterator<'a, I> { + type Item = (Action, Vec<&'a [Transition]>); + + fn next(&mut self) -> Option { + let len = self.iters.len(); + let (first_a, first_t) = self.iters.first_mut().and_then(|it| it.next())?; + let mut first_a = first_a; + let mut vals = vec![first_t; len]; + + let mut total = 1; + let mut i = 0; + while total < len { + i = (i + 1) % len; + let (next_a, next_t) = self + .iters + .get_mut(i) + .expect("i < len") + .find(|(a, _)| *a >= first_a)?; + if next_a > first_a { + first_a = next_a; + total = 1; + } else { + total += 1; + } + vals[i] = next_t; + } + Some((first_a, vals)) + } +} + /// Representation of a PG that can be executed transition-by-transition. /// /// The structure of the PG cannot be changed, @@ -338,84 +386,78 @@ impl<'def> ProgramGraphRun<'def> { pub fn possible_transitions( &self, ) -> impl Iterator>)> { - self.current_states - .first() - .into_iter() - .flat_map(|loc| { + let mut last_post_state: Option = None; + let iters = self + .current_states + .iter() + .map(|loc| { self.def.locations[loc.0 as usize] .0 .iter() - .map(|&(action, ..)| action) + .map(|(action, transitions)| (*action, transitions.as_slice())) }) - .chain( - self.current_states - .is_empty() - .then(|| (0..self.def.effects.len() as ActionIdx).map(Action)) - .into_iter() - .flatten(), - ) - .map(|action| (action, self.possible_transitions_action(action))) - } - - #[inline] - fn possible_transitions_action( - &self, - action: Action, - ) -> impl Iterator> { - self.current_states - .iter() - .map(move |&loc| self.possible_transitions_action_loc(action, loc)) - } - - fn possible_transitions_action_loc( - &self, - action: Action, - current_state: Location, - ) -> impl Iterator { - let mut last_post_state: Option = None; - self.def.locations[current_state.0 as usize] - .0 - .binary_search_by_key(&action, |&(a, ..)| a) - .into_iter() - .flat_map(move |action_idx| { - self.def.locations[current_state.0 as usize].0[action_idx] - .1 - .iter() - .filter_map(move |(post_state, guard, constraints)| { - // prevent post_states to be duplicated wastefully - if last_post_state.is_some_and(|s| s == *post_state) { - return None; - } - let (_, ref invariants) = self.def.locations[post_state.0 as usize]; - if if action == EPSILON { - self.active_autonomous_transition( - guard.as_ref(), - constraints, - invariants, - ) - } else { - match self.def.effects[action.0 as usize] { - Effect::Effects(_, ref resets) => self.active_transition( + .collect::>(); + TransitionsIterator::new(iters).map(move |(action, loc_transitions)| { + ( + action, + loc_transitions.into_iter().map(move |transitions| { + transitions + .iter() + .filter_map(move |(post_state, guard, constraints)| { + // prevent post_states to be duplicated wastefully + if last_post_state.is_some_and(|s| s == *post_state) { + return None; + } + let (_, ref invariants) = self.def.locations[post_state.0 as usize]; + if if action == EPSILON { + self.active_autonomous_transition( guard.as_ref(), constraints, invariants, - resets, - ), - Effect::Send(_) | Effect::Receive(_) => self - .active_autonomous_transition( + ) + } else { + match self.def.effects[action.0 as usize] { + Effect::Effects(_, ref resets) => self.active_transition( guard.as_ref(), constraints, invariants, + resets, ), + Effect::Send(_) | Effect::Receive(_) => self + .active_autonomous_transition( + guard.as_ref(), + constraints, + invariants, + ), + } + } { + last_post_state = Some(*post_state); + last_post_state + // Some(*post_state) + } else { + None } - } { - last_post_state = Some(*post_state); - last_post_state - } else { - None - } - }) - }) + }) + }), + ) + }) + // self.current_states + // .first() + // .into_iter() + // .flat_map(|loc| { + // self.def.locations[loc.0 as usize] + // .0 + // .iter() + // .map(|&(action, ..)| action) + // }) + // .chain( + // self.current_states + // .is_empty() + // .then(|| (0..self.def.effects.len() as ActionIdx).map(Action)) + // .into_iter() + // .flatten(), + // ) + // .map(|action| (action, self.possible_transitions_action(action))) } pub(crate) fn nosync_possible_transitions( @@ -480,7 +522,7 @@ impl<'def> ProgramGraphRun<'def> { ) -> bool { guard.is_none_or(|guard| { // TODO FIXME: is there a way to avoid creating a dummy RNG? - guard.eval(&|var| self.vars[var.0 as usize], &mut DummyRng) + guard.eval::(&|var| self.vars[var.0 as usize], &mut None) }) && constraints.iter().all(|(c, l, u)| { let time = self.clocks[c.0 as usize]; l.is_none_or(|l| l <= time) && u.is_none_or(|u| time < u) @@ -503,7 +545,7 @@ impl<'def> ProgramGraphRun<'def> { ) -> bool { guard.is_none_or(|guard| { // TODO FIXME: is there a way to avoid creating a dummy RNG? - guard.eval(&|var| self.vars[var.0 as usize], &mut DummyRng) + guard.eval::(&|var| self.vars[var.0 as usize], &mut None) }) && constraints.iter().chain(invariants).all(|(c, l, u)| { let time = self.clocks[c.0 as usize]; l.is_none_or(|l| l <= time) && u.is_none_or(|u| time < u) @@ -578,6 +620,7 @@ impl<'def> ProgramGraphRun<'def> { } else if let Effect::Effects(ref effects, ref resets) = self.def.effects[action.0 as usize] { if self.active_transitions(action, post_states, resets) { + let rng = &mut Some(rng); effects.iter().for_each(|(var, effect)| { self.vars[var.0 as usize] = effect.eval(&|var| self.vars[var.0 as usize], rng) }); @@ -631,6 +674,7 @@ impl<'def> ProgramGraphRun<'def> { Err(PgError::NotSend(action)) } else if self.active_transitions(action, post_states, &[]) { if let Effect::Send(effects) = &self.def.effects[action.0 as usize] { + let rng = &mut Some(rng); let vals = effects .iter() .map(|effect| effect.eval(&|var| self.vars[var.0 as usize], rng)) @@ -682,43 +726,6 @@ impl<'def> ProgramGraphRun<'def> { Err(PgError::UnsatisfiedGuard) } } - - #[inline] - pub(crate) fn eval(&self, expr: &Expression) -> Val { - expr.eval( - &|v: &Var| *self.vars.get(v.0 as usize).unwrap(), - &mut DummyRng, - ) - } - - #[inline] - pub(crate) fn val(&self, var: Var) -> Result { - self.vars - .get(var.0 as usize) - .copied() - .ok_or(PgError::MissingVar(var)) - } -} - -impl<'def> ProgramGraphRun<'def> { - pub(crate) fn montecarlo(&mut self, rng: &mut R) -> Option { - let mut rand = R::from_rng(rng); - if let Some((action, post_states)) = self - .possible_transitions() - .filter_map(|(action, post_state)| { - post_state - .map(|locs| locs.choose(rng)) - .collect::>>() - .map(|loc| (action, loc)) - }) - .choose(&mut rand) - { - self.transition(action, post_states.as_slice(), rng) - .expect("successful transition"); - return Some(action); - } - None - } } #[cfg(test)] diff --git a/scan_core/src/tracer.rs b/scan_core/src/tracer.rs new file mode 100644 index 0000000..79c4e3c --- /dev/null +++ b/scan_core/src/tracer.rs @@ -0,0 +1,34 @@ +use std::fs::File; + +use flate2::write::GzEncoder; + +use crate::{ + Time, Val, + channel_system::{Action, Event}, +}; + +/// A writer for traces +pub type TraceWriter = GzEncoder; + +/// Trait that handles streaming of traces, +/// e.g., to print them to file. +pub trait Tracer { + /// The extension to use for files of traces produced by the [`Tracer`]. + const EXTENSION: &str; + + /// Underlying model data to be traced. + type ModelData; + + /// Creates and initializes the Tracer + fn init(writer: TraceWriter, data: &Self::ModelData) -> Self; + + /// Stream a new state of the trace. + fn trace( + &mut self, + data: &Self::ModelData, + action: Action, + event: &Event, + time: Time, + ports: &[Vec], + ); +} diff --git a/scan_core/src/transition_system.rs b/scan_core/src/transition_system.rs index 8d746ba..5545b05 100644 --- a/scan_core/src/transition_system.rs +++ b/scan_core/src/transition_system.rs @@ -1,90 +1,197 @@ -use crate::{Oracle, RunOutcome, Time, Val}; -use log::trace; -use std::sync::{ - Arc, - atomic::{AtomicBool, Ordering}, -}; +use std::sync::Arc; +use std::sync::atomic::{AtomicBool, Ordering}; -/// Trait that handles streaming of traces, -/// e.g., to print them to file. -pub trait Tracer { - /// Initialize new streaming. - /// - /// This method needs to be called once, before calls to [`Self::trace`]. - fn init(&mut self); +use log::trace; +use rand::rngs::SmallRng; - /// Stream a new state of the trace. - fn trace>(&mut self, action: &A, time: Time, ports: I); +use crate::channel_system::{ + Action, Channel, ChannelSystem, ChannelSystemBuilder, ChannelSystemRun, Event, EventType, +}; +use crate::{BooleanExpr, Oracle, RunOutcome, Time, Tracer, Val}; + +/// An atomic variable exposed by the [`ChannelSystem to the TransitionSystem`]. +#[derive(Debug, Clone, Copy)] +pub enum Atom { + /// A predicate. + State(Channel, usize), + /// A send event. + Event(Channel), +} - /// Finalize and close streaming. - /// - /// This method needs to be called at the end of the execution. - fn finalize(self, outcome: &RunOutcome); +/// A definition type that instances new [`CsModelRun`]. +#[derive(Debug, Clone)] +pub struct TransitionSystem { + cs: ChannelSystem, + // ports are supposed to be ordered by channel + ports: Vec, + vals: Vec>, + predicates: Vec>, } -// Dummy Tracer that does nothing -impl Tracer for () { - fn init(&mut self) {} +impl TransitionSystem { + /// Creates a new [`CsModel`] from a [`ChannelSystemBuilder`]. + pub fn new(cs: ChannelSystemBuilder) -> Self { + let cs = cs.build(); + Self { + ports: Vec::new(), + vals: Vec::new(), + cs, + predicates: Vec::new(), + } + } - fn trace>(&mut self, _action: &A, _time: Time, _ports: I) {} + /// Adds a new port to the [`CsModel`], + /// which is given by an [`Channel`] and a default [`Val`] value. + pub fn add_port(&mut self, channel: Channel, mut value: Vec) { + let len = self.cs.channels()[u16::from(channel) as usize].0.len(); + assert_eq!(len, value.len()); + // TODO FIXME: error handling and type checking. + // Keep ports list ordered + // Don't insert duplicated ports + if let Err(index) = self.ports.binary_search(&channel) { + self.ports.insert(index, channel); + value.shrink_to_fit(); + self.vals.insert(index, value); + } + assert!(self.ports.is_sorted()); + assert_eq!(self.ports.len(), self.vals.len()); + } - fn finalize(self, _outcome: &RunOutcome) {} -} + /// Adds a new predicate to the [`CsModel`], + /// which is an expression over the CS's channels. + pub fn add_predicate(&mut self, predicate: BooleanExpr) { + // Make sure predicate type-checks + let _ = predicate.eval::( + &|port| match port { + Atom::State(channel, idx) => { + let index = self + .ports + .binary_search(&channel) + .expect("port must have been initialized"); + self.vals[index][idx] + } + Atom::Event(..) => Val::Boolean(false), + }, + &mut None, + ); + self.predicates.push(predicate); + } -/// A type that can generate instances of a [`TransitionSystem`]. -pub trait TransitionSystemGenerator { - /// The type of [`TransitionSystem`] to be generated. - type Ts<'a>: TransitionSystem - where - Self: 'a; + /// Shrink ports storage to optimize space use. + /// To be called after having added all ports. + pub fn shrink(&mut self) { + self.ports.shrink_to_fit(); + self.vals.shrink_to_fit(); + } - /// Generate a new instance of the [`TransitionSystem`]. - fn generate<'a>(&'a self) -> Self::Ts<'a>; + /// Generates an executable run of the model. + pub fn new_run(&self) -> TransitionSystemRun<'_> { + let mut vals = self.vals.clone(); + vals.shrink_to_fit(); + TransitionSystemRun { + cs: self.cs.new_instance(), + ports: &self.ports, + vals, + predicates: &self.predicates, + last_event: None, + } + } } -/// Trait for types that can execute like a transition system. +/// Transition system model based on a [`ChannelSystem`]. /// -/// Together with an [`Oracle`], it provides a verifiable system. -pub trait TransitionSystem { - /// The type of events produced by the execution of the system. - type Event; +/// It is essentially a CS which keeps track of the [`Event`]s produced by the execution +/// and determining a set of predicates. +#[derive(Debug, Clone)] +pub struct TransitionSystemRun<'def> { + cs: ChannelSystemRun<'def>, + ports: &'def [Channel], + vals: Vec>, + predicates: &'def [BooleanExpr], + last_event: Option<(Action, Event)>, +} - /// Performs a (random) transition on the [`TransitionSystem`] and returns the raised `Event`, - /// unless the execution is terminated and no further events can happen. - fn transition(&mut self) -> Option; +impl<'def> TransitionSystemRun<'def> { + /// Perform a random transition. + /// + /// Used to generate Montecarlo-like executions + pub fn transition(&mut self) { + self.last_event = self.cs.montecarlo_execution(); + if let Some((_, ref event)) = self.last_event + && let EventType::Send(ref vals) = event.event_type + && let Ok(index) = self.ports.binary_search(&event.channel) + { + // Since we have to update old values, + // the vectors are already allocated and their is always the same. + // Copying from slice should be faster than cloning. + self.vals[index].copy_from_slice(vals); + } + } - /// Current time of the [`TransitionSystem`] (for timed systems). - fn time(&self) -> Time; + /// Returns last event processed by model. + #[inline] + pub fn last_event(&self) -> Option<&(Action, Event)> { + self.last_event.as_ref() + } - /// Increase current time of the [`TransitionSystem`] (for timed systems). - fn time_tick(&mut self); + #[inline] + fn time(&self) -> Time { + self.cs.time() + } - /// The current values of the [`TransitionSystem`]'s labels. - fn labels(&self) -> impl Iterator; + #[inline] + fn time_tick(&mut self) { + self.cs.wait(1).expect("time error") + } - /// The current internal state of the [`TransitionSystem`]. - fn state(&self) -> impl Iterator; + fn labels(&self) -> impl Iterator { + self.predicates.iter().map(|prop| { + prop.eval::( + &|port| match port { + Atom::State(channel, idx) => { + let port_idx = self + .ports + .binary_search(&channel) + .expect("port must exist and be initialized"); + self.vals[port_idx][idx] + } + Atom::Event(channel) => { + Val::Boolean(self.last_event.as_ref().is_some_and(|(_, e)| { + e.channel == channel && matches!(e.event_type, EventType::Send(..)) + })) + } + }, + &mut None, + ) + }) + } + + #[inline] + fn state(&self) -> &[Vec] { + &self.vals + } /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] and returns a [`RunOutcome`]. - fn experiment( + pub(crate) fn experiment( &mut self, duration: Time, mut oracle: O, running: Arc, ) -> RunOutcome { trace!("new run starting"); - let mut time; // reuse vector to avoid allocations - let mut labels = Vec::new(); + let mut labels = Vec::from_iter(self.labels()); + // Initialize oracle with TS initial state + oracle.update_state(&labels); while self.time() <= duration { - if let Some(_event) = self.transition() { + self.transition(); + if self.last_event().is_some() { labels.clear(); labels.extend(self.labels()); oracle.update_state(&labels); } else { self.time_tick(); - time = self.time(); - oracle.update_time(time); + oracle.update_time(self.time()); } if !running.load(Ordering::Relaxed) { trace!("run stopped"); @@ -102,31 +209,37 @@ pub trait TransitionSystem { /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] /// and process the execution trace via the given [`Tracer`]. - fn trace(&mut self, duration: Time, mut oracle: O, mut tracer: T) + pub(crate) fn trace( + &mut self, + duration: Time, + mut oracle: O, + mut tracer: T, + model_data: &T::ModelData, + ) -> RunOutcome where - T: Tracer, + T: Tracer, { - // let mut current_len = 0; trace!("new run starting"); - let mut time; // reuse vector to avoid allocations - let mut labels = Vec::new(); - tracer.init(); + let mut labels = Vec::from_iter(self.labels()); + // Initialize oracle with TS initial state + oracle.update_state(&labels); + // WARN FIXME TODO: Initial state is not written as there is no corresponding action/event + // Same issue for time-tick events while self.time() <= duration { - if let Some(event) = self.transition() { + self.transition(); + if let Some((action, event)) = self.last_event() { + tracer.trace(model_data, *action, event, self.time(), self.state()); labels.clear(); labels.extend(self.labels()); - time = self.time(); - tracer.trace(&event, time, self.state()); oracle.update_state(&labels); } else { self.time_tick(); - time = self.time(); - oracle.update_time(time); + oracle.update_time(self.time()); } } trace!("run complete"); let verified = Vec::from_iter(oracle.final_output_guarantees()); - tracer.finalize(&RunOutcome::Verified(verified)); + RunOutcome::Verified(verified) } } diff --git a/scan_core/tests/counter.rs b/scan_core/tests/counter.rs index 6380a47..ed2b80e 100644 --- a/scan_core/tests/counter.rs +++ b/scan_core/tests/counter.rs @@ -1,12 +1,14 @@ -use scan_core::{program_graph::*, *}; +use scan_core::{channel_system::ChannelSystemBuilder, *}; #[test] -fn counter_pg() -> Result<(), PgError> { - let mut pg = ProgramGraphBuilder::new(); - let initial = pg.new_initial_location(); - let action = pg.new_action(); - let var = pg.new_var(Val::Integer(0))?; - pg.add_effect( +fn counter_pg() { + let mut cs = ChannelSystemBuilder::new(); + let pg = cs.new_program_graph(); + let initial = cs.new_initial_location(pg).expect("new initial location"); + let action = cs.new_action(pg).expect("new action"); + let var = cs.new_var(pg, Val::Integer(0)).expect("new var"); + cs.add_effect( + pg, action, var, (Expression::from_var(var, Type::Integer) + Expression::from(Val::Integer(1))).unwrap(), @@ -18,11 +20,13 @@ fn counter_pg() -> Result<(), PgError> { Expression::from(Val::Integer(counter)), ) .unwrap(); - pg.add_transition(initial, action, initial, Some(guard)) + cs.add_transition(pg, initial, action, initial, Some(guard)) .unwrap(); } - let pg = PgModel::new(pg, Vec::new(), Vec::new()); - let mut pg: PgModelRun = pg.generate(); - while pg.transition().is_some() {} - Ok(()) + let cs = TransitionSystem::new(cs); + let mut pg: TransitionSystemRun = cs.new_run(); + pg.transition(); + while pg.last_event().is_some() { + pg.transition(); + } } diff --git a/scan_jani/Cargo.toml b/scan_jani/Cargo.toml index d970278..20f0665 100644 --- a/scan_jani/Cargo.toml +++ b/scan_jani/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "smc_scan_jani" -version = "0.1.1" +version = "0.2.0" edition = "2024" description = "JANI frontend for the Scan model checker." documentation = "https://convince-project.github.io/scan/crates/scan_jani/index.html" @@ -9,19 +9,25 @@ repository = "https://github.com/convince-project/scan" license = "Apache-2.0" readme = "README.md" keywords = ["verification", "model-checking", "jani"] -categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] [lib] name = "scan_jani" # The name of the target. -crate-type = ["lib"] # The crate types to generate. +crate-type = ["lib"] # The crate types to generate. [dependencies] anyhow = { workspace = true } log = { workspace = true } -smc_scan_core = {version = "0.1.1", path="../scan_core" } +smc_scan_core = { version = "0.2.0", path = "../scan_core" } +smc_scan_mtl = { version = "0.1.0", path = "../scan_mtl" } thiserror = { workspace = true } serde = { workspace = true } serde_json = { workspace = true } either = "1.15.0" csv = { workspace = true } -flate2 = { workspace = true } diff --git a/scan_jani/src/builder.rs b/scan_jani/src/builder.rs index 7508122..42ffa7d 100644 --- a/scan_jani/src/builder.rs +++ b/scan_jani/src/builder.rs @@ -1,20 +1,20 @@ use super::Model; use crate::parser::{ - self, Automaton, BoolOp, ConstantDeclaration, Destination, Edge, Expression, Guard, Location, - NumCompOp, PropertyExpression, Sync, VariableDeclaration, + self, Automaton, BoolOp, ConstantDeclaration, Destination, Edge, Expression, + PropertyExpression, Sync, VariableDeclaration, }; use anyhow::{Context, anyhow, bail}; use either::Either; use scan_core::{ - BooleanExpr, FloatExpr, Mtl, MtlOracle, PgModel, Type, TypeError, Val, - program_graph::{self, Action, PgExpression, ProgramGraphBuilder, Var}, -}; -use std::{ - collections::{BTreeMap, HashMap, HashSet}, - ops::Not, + Atom, BooleanExpr, Float, FloatExpr, Integer, IntegerExpr, Natural, NaturalExpr, + TransitionSystem, Type, TypeError, Val, + channel_system::{Action, Channel, ChannelSystemBuilder, CsExpression, Location, PgId, Var}, }; +use scan_mtl::{Mtl, MtlOracle}; +use serde::de::IgnoredAny; +use std::collections::HashMap; -#[derive(Clone)] +#[derive(Debug, Clone)] pub struct JaniModelData { pub actions: HashMap, pub ports: Vec<(String, Type)>, @@ -24,89 +24,658 @@ pub struct JaniModelData { pub(crate) fn build( jani_model: Model, properties: &[String], -) -> anyhow::Result<(PgModel, MtlOracle, JaniModelData)> { +) -> anyhow::Result<(TransitionSystem, MtlOracle, JaniModelData)> { let builder = JaniBuilder::default(); builder.build(jani_model, properties) } -#[derive(Default)] +#[derive(Default, Debug, Clone)] struct JaniBuilder { - system_actions: HashMap, + system_actions: HashMap, // Associating name to variable, initial value and type. - global_vars: BTreeMap, + global_state_channel: Option, + global_vars: HashMap, + global_state_vec: Vec, global_constants: HashMap, + automaton_builders: Vec, +} + +#[derive(Debug, Clone)] +struct AutomatonBuilder { + // tracks locations and their "idle" side-location + locations: HashMap, + local_vars: HashMap, + idle_locations: HashMap, + return_location: Location, + // assign action name -> cs base action + destination actions + dest_actions: HashMap< + // triggering sync action + Action, + Vec<( + // dest action + Action, + // dest location + Location, + )>, + >, + rng: Var, + current_loc: Var, +} + +impl AutomatonBuilder { + fn new(rng: Var, current_loc: Var, return_location: Location) -> Self { + AutomatonBuilder { + locations: HashMap::new(), + local_vars: HashMap::new(), + dest_actions: HashMap::new(), + rng, + current_loc, + idle_locations: HashMap::new(), + return_location, + } + } } +// TRANSITIONS DECOMPOSITION +// +// [pre_location] +// | edge guard | sync_action: unset transient vars +// [edge_location] <> previous automata dest_actions +// | dest probability guard | dest_action: set current_location + dest assignments + set transient_vars +// [dest_location] <> successive automata dest_actions +// | system_action: send global vars +// [post_location] + impl JaniBuilder { - const RNG: &str = "__RNG__"; - const GEN: &str = "__GEN__"; + const SILENT: &str = "__SILENT__"; const INITIAL: &str = "__INITIAL__"; pub(crate) fn build( mut self, - mut jani_model: Model, + jani_model: Model, properties: &[String], - ) -> anyhow::Result<(PgModel, MtlOracle, JaniModelData)> { - // WARN Necessary "normalization" process - self.init(&mut jani_model)?; - self.normalize(&mut jani_model) - .context("JANI normalization pre-process fails")?; - - let mut pgb = ProgramGraphBuilder::new(); - - jani_model.system.syncs.iter().for_each(|sync| { - let result = sync.result.as_ref().expect("no silent actions"); - if !self.system_actions.contains_key(result) { - let action = pgb.new_action(); - let prev = self.system_actions.insert(result.clone(), action); - assert!(prev.is_none(), "checked by above if condition"); - } - }); + ) -> anyhow::Result<(TransitionSystem, MtlOracle, JaniModelData)> { + let mut cs = ChannelSystemBuilder::new(); + let pg_id = cs.new_program_graph(); + let automata: HashMap<&str, &Automaton> = jani_model + .automata + .iter() + .map(|automaton| (automaton.name.as_str(), automaton)) + .collect(); jani_model .constants .iter() .try_for_each(|c| self.add_global_constant(c))?; - jani_model - .variables - .iter() - .try_for_each(|var| self.add_global_var(&mut pgb, var))?; - jani_model - .system - .elements - .iter() - .enumerate() - .try_for_each(|(e_idx, element)| { - let automaton = jani_model - .automata + let global_state_len = jani_model.variables.len(); + let mut global_state_init = Vec::with_capacity(global_state_len); + let mut global_state_type = Vec::with_capacity(global_state_len); + let mut global_state_expr = Vec::with_capacity(global_state_len); + + // Create global variables + for variable_dec in jani_model.variables.iter() { + let var_type = (&variable_dec.r#type).try_into().expect("convert type"); + let init = variable_dec + .initial_value + .as_ref() + .map(|expr| self.build_expression(expr, Some(var_type), &self.global_vars)) + .transpose()? + .unwrap_or_else(|| CsExpression::from(var_type.default_value())); + let val = init.eval_constant()?; + if var_type != val.r#type() { + bail!( + "system variable {} initialization value wrong type", + variable_dec.name + ); + } + + let var = cs.new_var(pg_id, val)?; + self.global_vars + .insert(variable_dec.name.clone(), (var, val, var_type)); + self.global_state_vec.push(variable_dec.name.clone()); + global_state_type.push(var_type); + global_state_init.push(val); + global_state_expr.push(CsExpression::from_var(var, var_type)); + } + + // Create channel to send global state expression to + let global_state_channel = cs.new_sink(global_state_type); + self.global_state_channel = Some(global_state_channel); + + // for every system action (including silent ones), + // create action which sends global state to channel + for system_action in &jani_model.actions { + let system_action_id = + cs.new_send(pg_id, global_state_channel, global_state_expr.clone())?; + self.system_actions + .insert(system_action.name.clone(), system_action_id); + } + let silent_system_action = + cs.new_send(pg_id, global_state_channel, global_state_expr.clone())?; + // Add initialization action + let system_initial_action_id = + cs.new_send(pg_id, global_state_channel, global_state_expr)?; + self.system_actions + .insert(Self::INITIAL.to_string(), system_initial_action_id); + + for element in jani_model.system.elements.iter() { + let rng = cs.new_var(pg_id, Val::from(0.)).expect("new var"); + let current_loc = cs.new_var(pg_id, Val::from(0 as Natural)).expect("new var"); + let return_location = cs.new_location(pg_id).expect("new location"); + + let mut automaton_builder = AutomatonBuilder::new(rng, current_loc, return_location); + let automaton = automata + .get(element.automaton.as_str()) + .ok_or_else(|| anyhow!("missing automaton {}", element.automaton))?; + + // initial locations + let initial = cs.new_initial_location(pg_id).expect("initial location"); + assert!(automaton_builder.locations.is_empty()); + automaton_builder + .locations + .insert(Self::INITIAL.to_string(), (initial, 0)); + + // create locations + for location in &automaton.locations { + let loc = cs.new_location(pg_id).expect("new location"); + // Give every location an ID unique within the automaton + // (not necessarily globally unique) + let loc_id = automaton_builder.locations.len() as Natural; + automaton_builder + .locations + .insert(location.name.clone(), (loc, loc_id)); + let dest_guard = BooleanExpr::NatEqual( + scan_core::NaturalExpr::from(loc_id), + scan_core::NaturalExpr::Var(current_loc), + ); + cs.add_autonomous_transition(pg_id, return_location, loc, Some(dest_guard)) + .expect("add transition"); + } + + // Add local variables + automaton + .variables + .iter() + .try_for_each(|var| { + self.add_local_var(&mut cs, pg_id, var, &mut automaton_builder.local_vars) + }) + .context("failed adding local variables")?; + + self.automaton_builders.push(automaton_builder); + } + + // Extend system syncs with async silent actions + // for each element that has an edge activated by silent action + let num_elements = jani_model.system.elements.len(); + assert_eq!(self.automaton_builders.len(), num_elements); + let silent_syncs = (0..num_elements) + .filter(|&n| { + let element = jani_model.system.elements.get(n).unwrap(); + let automaton = automata.get(element.automaton.as_str()).expect("automaton"); + automaton.edges.iter().any(|edge| edge.action.is_none()) + }) + .map(|n| { + let mut synchronise = vec![None; num_elements]; + synchronise[n] = Some(Self::SILENT.to_string()); + parser::Sync { + synchronise, + result: None, + _comment: IgnoredAny, + } + }); + // Sync calling initial action on all elements + let initial_sync = Sync { + synchronise: vec![Some(Self::INITIAL.to_string()); jani_model.system.elements.len()], + result: Some(Self::INITIAL.to_string()), + _comment: IgnoredAny, + }; + + // for every sync, create sync action + for sync in silent_syncs + .chain(jani_model.system.syncs) + .chain(std::iter::once(initial_sync)) + { + let sync_action = cs.new_action(pg_id).expect("new action"); + let system_action = sync + .result + .as_ref() + .map(|result| { + self.system_actions + .get(result) + .ok_or_else(|| anyhow!("sync result {result} unknown")) + }) + .transpose()? + .copied() + .unwrap_or(silent_system_action); + + // elements unaffected by sync must ignore the sync action in every location + // by moving to idle location + let mut any_unaffected = false; + for (element_idx, _) in sync + .synchronise + .iter() + .enumerate() + .filter(|(_, action)| action.is_none()) + { + any_unaffected = true; + let automaton_builder = self + .automaton_builders + .get_mut(element_idx) + .expect("automaton builder"); + + // Create idle location for this sync/automaton + let sync_idle_location = cs.new_location(pg_id).expect("new location"); + automaton_builder + .idle_locations + .insert(sync_action, sync_idle_location); + cs.add_transition( + pg_id, + sync_idle_location, + system_action, + automaton_builder.return_location, + None, + ) + .expect("add transition"); + + for (location, loc_id) in automaton_builder.locations.values() { + // Skip initial location (not needed) + if *loc_id == 0 { + continue; + } + cs.add_transition(pg_id, *location, sync_action, sync_idle_location, None) + .expect("add transition"); + } + } + + // For every element involved in the sync action, + // build transitions associated to relevant edges + for (element_idx, element, automaton_action) in jani_model + .system + .elements + .iter() + .zip(&sync.synchronise) + .enumerate() + .filter_map(|(element_idx, (element, action))| { + action.as_ref().map(|action| (element_idx, element, action)) + }) + { + let automaton = automata + .get(element.automaton.as_str()) + .ok_or_else(|| anyhow!("missing automaton {}", element.automaton))?; + + let automaton_builder = self + .automaton_builders + .get(element_idx) + .expect("automaton builder"); + + // Sync actions randomize automaton's RNG + cs.add_effect( + pg_id, + sync_action, + automaton_builder.rng, + CsExpression::Float(FloatExpr::Rand(Box::new(( + FloatExpr::from(0.), + FloatExpr::from(1.), + )))), + ) + .expect("add effect"); + + let initial_edge = Edge { + location: Self::INITIAL.to_string(), + action: Some(Self::INITIAL.to_string()), + guard: None, + destinations: automaton + .initial_locations + .iter() + .map(|location| Destination { + location: location.clone(), + probability: None, + assignments: Vec::new(), + _comment: IgnoredAny, + }) + .collect(), + _comment: IgnoredAny, + }; + + let initial_location = parser::Location { + name: Self::INITIAL.to_string(), + transient_values: Vec::new(), + _comment: IgnoredAny, + }; + + // create edges for the automaton action corresponding to the sync action + for edge in automaton + .edges .iter() - .find(|a| a.name == element.automaton) - .ok_or(anyhow!( - "element '{}' is not a known automaton", - element.automaton - ))?; - self.build_automaton(&jani_model, &mut pgb, automaton, e_idx) - .with_context(|| format!("failed to build automaton '{}'", element.automaton)) - })?; + .chain(std::iter::once(&initial_edge)) + .filter(|edge| { + edge.action.as_deref().unwrap_or(Self::SILENT) == automaton_action + }) + { + let automaton_builder = self + .automaton_builders + .get(element_idx) + .expect("automaton builder"); + let (pre_loc, _) = *automaton_builder + .locations + .get(&edge.location) + .ok_or_else(|| { + anyhow!( + "missing location {} in automaton {}", + edge.location, + element.automaton + ) + })?; + + // Sync actions initiate a transition so they need to reset transient variables + // WARN: We assume that no other automaton is setting the same transient global variables, + // so that resetting all of them at the level of sync action is consistent with expected behavior. + for transient in &automaton + .locations + .iter() + .chain(std::iter::once(&initial_location)) + .find(|loc| loc.name == edge.location) + .ok_or_else(|| anyhow!("edge location {} not found", edge.location))? + .transient_values + { + let (var, init, _) = automaton_builder + .local_vars + .get(&transient.r#ref) + .or_else(|| self.global_vars.get(&transient.r#ref)) + .ok_or_else(|| { + anyhow!("transient value {} not found", transient.r#ref) + })?; + cs.add_effect(pg_id, sync_action, *var, CsExpression::from(*init)) + .expect("set transient value"); + } + + // Transition to edge location + let edge_location = cs.new_location(pg_id).expect("new location"); + let guard = edge + .guard + .as_ref() + .map(|guard| { + self.build_expression( + &guard.exp, + Some(Type::Boolean), + &automaton_builder.local_vars, + ) + .and_then(|guard| { + if let CsExpression::Boolean(guard) = guard { + Ok(guard) + } else { + Err(anyhow!("guard is not a boolean expression")) + } + }) + }) + .transpose() + .with_context(|| { + format!( + "failed creating guard expression for edge in automaton {}", + automaton.name + ) + })?; + + // NOTE: different edges can have the same sync action + // and a non-deterministic choice of edge location + cs.add_transition(pg_id, pre_loc, sync_action, edge_location, guard) + .expect("add transition"); + + // consider previous occurrences of transitions triggered by same sync action + // and allow them to execute first while current automaton sits on edge_location + for prev_automaton_builder in &mut self.automaton_builders[..element_idx] { + if let Some(v) = prev_automaton_builder.dest_actions.get(&sync_action) { + for (prev_dest_action, _prev_dest_location) in v.iter() { + // for the same sync_action, add previous dest_actions loops in edge_location + cs.add_transition( + pg_id, + edge_location, + *prev_dest_action, + edge_location, + None, + ) + .expect("add transition"); + } + } + } + + let mut prob_lower_bound: Option> = None; + + for dest in edge.destinations.iter() { + let dest_action = cs.new_action(pg_id)?; + let dest_location = cs.new_location(pg_id).expect("new location"); + + let automaton_builder = self + .automaton_builders + .get(element_idx) + .expect("automaton builder"); + + // add effects + for assignment in &dest.assignments { + let (var, _, r#type) = automaton_builder + .local_vars + .get(&assignment.r#ref) + .or_else(|| self.global_vars.get(&assignment.r#ref)) + .ok_or_else(|| anyhow!("unknown variable {}", assignment.r#ref))?; + let effect = self + .build_expression( + &assignment.value, + Some(*r#type), + &automaton_builder.local_vars, + ) + .with_context(|| { + format!( + "failed building expression for assignment of variable {}", + assignment.r#ref + ) + })?; + cs.add_effect(pg_id, dest_action, *var, effect) + .expect("add effect"); + } + + // dest actions need to also set transient variables of destination + for transient in &automaton + .locations + .iter() + .find(|loc| loc.name == dest.location) + .ok_or_else(|| { + anyhow!("transition destination {} not found", dest.location) + })? + .transient_values + { + let (var, _, r#type) = automaton_builder + .local_vars + .get(&transient.r#ref) + .or_else(|| self.global_vars.get(&transient.r#ref)) + .ok_or_else(|| { + anyhow!("transient value {} not found", transient.r#ref) + })?; + let effect = self.build_expression( + &transient.value, + Some(*r#type), + &automaton_builder.local_vars, + )?; + cs.add_effect(pg_id, dest_action, *var, effect) + .expect("set transient value"); + } + + let prob_expr; + if let Some(ref prob) = dest.probability { + let probability; + if let scan_core::Expression::Float(prob) = self.build_expression( + &prob.exp, + Some(Type::Float), + &automaton_builder.local_vars, + )? { + probability = prob; + } else { + bail!("probability is not a float expression"); + } + if let Some(prob_lower_bound) = prob_lower_bound.as_mut() { + let prob_upper_bound = prob_lower_bound.clone() + probability; + prob_expr = Some( + BooleanExpr::FloatLessEq( + prob_lower_bound.clone(), + FloatExpr::Var(automaton_builder.rng), + ) & BooleanExpr::FloatLess( + FloatExpr::Var(automaton_builder.rng), + prob_upper_bound.clone(), + ), + ); + *prob_lower_bound = prob_upper_bound; + } else { + prob_expr = Some(BooleanExpr::FloatLess( + FloatExpr::Var(automaton_builder.rng), + probability.clone(), + )); + prob_lower_bound = Some(probability); + } + } else { + if let Some(prob_lower_bound) = prob_lower_bound.as_mut() { + prob_expr = Some(BooleanExpr::FloatLessEq( + prob_lower_bound.clone(), + FloatExpr::Var(automaton_builder.rng), + )); + *prob_lower_bound = FloatExpr::Const(1.0); + } else { + prob_expr = None; + } + } + cs.add_transition( + pg_id, + edge_location, + dest_action, + dest_location, + prob_expr, + ) + .expect("add transition"); + + // consider previous occurrences of transitions triggered by same sync action + for prev_automaton_builder in &mut self.automaton_builders[..element_idx] { + if let Some(v) = prev_automaton_builder.dest_actions.get(&sync_action) { + for (_prev_dest_action, prev_dest_location) in v.iter() { + // add dest_action loop in previous dest_locations for the same sync_action + cs.add_transition( + pg_id, + *prev_dest_location, + dest_action, + *prev_dest_location, + None, + ) + .expect("add transition"); + } + } + } + + // elements unaffected by sync must ignore the dest action in every idle location + for (automaton_builder, _) in self + .automaton_builders + .iter() + .zip(&sync.synchronise) + .filter(|(_, action)| action.is_none()) + { + let idle_loc = *automaton_builder + .idle_locations + .get(&sync_action) + .expect("idle location"); + cs.add_transition(pg_id, idle_loc, dest_action, idle_loc, None) + .expect("add transition"); + } + + // need to borrow mutably now + let automaton_builder = self + .automaton_builders + .get_mut(element_idx) + .expect("automaton builder"); + + automaton_builder + .dest_actions + .entry(sync_action) + .or_default() + .push((dest_action, dest_location)); + + let (post_loc, post_loc_idx) = *automaton_builder + .locations + .get(&dest.location) + .ok_or_else(|| { + anyhow!( + "missing location {} in automaton {}", + dest.location, + element.automaton + ) + })?; + + cs.add_effect( + pg_id, + dest_action, + automaton_builder.current_loc, + CsExpression::from(post_loc_idx), + ) + .expect("set current location"); + + // Send global state to channel and transition to post location + if any_unaffected { + cs.add_transition( + pg_id, + dest_location, + system_action, + dest_location, + None, + ) + .expect("add location"); + cs.add_autonomous_transition(pg_id, dest_location, post_loc, None) + .expect("add location"); + } else { + cs.add_transition(pg_id, dest_location, system_action, post_loc, None) + .expect("add location"); + } + } + } + } + } + + let mut cs_model = TransitionSystem::new(cs); + // global state port, only one we need + cs_model.add_port(global_state_channel, global_state_init); // Add properties - let properties = jani_model + let properties = if properties.is_empty() { + jani_model + .properties + .iter() + .map(|p| p.name.clone()) + .collect() + } else { + properties.to_vec() + }; + + let property_exprs = jani_model .properties .iter() - .filter(|p| properties.is_empty() || properties.contains(&p.name)) + .filter(|p| properties.contains(&p.name)) .map(|p| { - self.build_property(&p.expression) - .map(|p| p.right_or_else(Mtl::Atom)) + self.build_property(&p.expression).and_then(|p| match p { + Either::Left(expr) => { + if let scan_core::Expression::Boolean(bexpr) = expr { + Ok(Mtl::Atom(bexpr)) + } else { + Err(anyhow!("predicate not a boolean expression")) + } + } + Either::Right(mtl) => Ok(mtl), + }) }) .collect::, _>>()?; - fn extract_predicates(prop: &Mtl) -> Vec { + fn extract_predicates( + prop: &Mtl>, + ) -> Vec> { match prop { Mtl::Atom(pred) => vec![pred.clone()], Mtl::Until(lhs, rhs) => vec![lhs.clone(), rhs.clone()], } } - fn extract_mtl(prop: &Mtl, idx: &mut usize) -> Mtl { + fn extract_mtl(prop: &Mtl>, idx: &mut usize) -> Mtl { match prop { Mtl::Atom(_) => { let prop = Mtl::Atom(*idx); @@ -122,288 +691,31 @@ impl JaniBuilder { } let mut idx = 0; let mut oracle = MtlOracle::default(); - properties + property_exprs .iter() - .map(|p| extract_mtl(p, &mut idx)) - .for_each(|mtl| oracle.add_guarantee(mtl)); - let predicates = properties + .flat_map(|prop| extract_predicates(prop).into_iter()) + .for_each(|predicate| { + cs_model.add_predicate(predicate); + }); + property_exprs .into_iter() - .flat_map(|prop| extract_predicates(&prop).into_iter()) - .collect::>(); - let global_vars = self - .global_vars - .values() - .map(|(var, ..)| var) - .copied() - .collect(); + .map(|p| extract_mtl(&p, &mut idx)) + .for_each(|mtl| oracle.add_guarantee(mtl)); // Finalize, build and return everything - let pg_model = PgModel::new(pgb, global_vars, predicates); - let data = self.data(jani_model); - Ok((pg_model, oracle, data)) - } - - fn init(&mut self, jani_model: &mut Model) -> anyhow::Result<()> { - // New initial action sync over all elements - let sync_initial = Sync { - synchronise: vec![Some(String::from(Self::INITIAL)); jani_model.system.elements.len()], - result: Some(String::from(Self::INITIAL)), - _comment: String::new(), - }; - jani_model.system.syncs.push(sync_initial); - - for automaton in &mut jani_model.automata { - // New "real" initial location, needed to instantiate automaton's initial locations - let gen_initial = Location { - name: String::from(Self::INITIAL), - transient_values: Vec::new(), - _comment: String::new(), - }; - automaton.locations.push(gen_initial); - - let init_edge = Edge { - location: String::from(Self::INITIAL), - action: Some(String::from(Self::INITIAL)), - guard: None, - destinations: automaton - .initial_locations - .iter() - .cloned() - .map(|location| Destination { - location, - probability: None, - assignments: Vec::new(), - _comment: String::new(), - }) - .collect(), - _comment: String::new(), - }; - automaton.edges.push(init_edge); - - // Replace initial location - automaton.initial_locations = vec![String::from(Self::INITIAL)]; - } - Ok(()) - } - - // An action in JANI doesn not carry effects, - // so we need to duplicate actions until each one has unique effects. - // The modified model is such that: - // - // - Every action has a unique set of assignments (duplicates actions). - // - Every edge has a unique destination (because destinations are tied to assignments). - // - Syncs are updated with new actions - // (if action a is duplicated to a', all syncs containing a are duplicated with a' and a new result - // so that result corresponds to a unique set of assignments, union of all the assignments of each of its actions). - // - Probability is encoded in guard - fn normalize(&mut self, jani_model: &mut Model) -> anyhow::Result<()> { - // index is global so there is no risk of name-clash - let mut idx = 0; - let rng = Expression::Identifier(String::from(Self::RNG)); - for automaton in &mut jani_model.automata { - let mut new_edges = Vec::new(); - for edge in &mut automaton.edges { - // Avoid silent actions - if edge.action.is_none() { - edge.action = Some(Self::GEN.to_string() + &idx.to_string()); - idx += 1; - } - let edge_action = edge.action.clone().expect("no silent action"); - assert!(!edge_action.is_empty()); - let mut prob: Option = None; - for dest in &mut edge.destinations { - // Add probability to guard - let mut guard_exp = edge.guard.as_ref().map(|guard| guard.exp.clone()); - if let Some(ref p) = dest.probability { - // First probability case has no lower bound - if let Some(ref prob) = prob { - let lower_bound = Expression::NumComp { - op: NumCompOp::Leq, - left: Box::new(prob.clone()), - right: Box::new(rng.clone()), - }; - guard_exp = guard_exp - .map(|g| Expression::Bool { - op: BoolOp::And, - left: Box::new(lower_bound.clone()), - right: Box::new(g), - }) - .or(Some(lower_bound)); - } - let upper_prob = prob.map_or_else( - || p.exp.clone(), - |prob| Expression::IntOp { - op: parser::IntOp::Plus, - left: Box::new(prob), - right: Box::new(p.exp.clone()), - }, - ); - let upper_bound = Expression::NumComp { - op: NumCompOp::Less, - left: Box::new(rng.clone()), - right: Box::new(upper_prob.clone()), - }; - guard_exp = guard_exp - .map(|g| Expression::Bool { - op: BoolOp::And, - left: Box::new(upper_bound.clone()), - right: Box::new(g), - }) - .or(Some(upper_bound)); - // Update accumulated probability - prob = Some(upper_prob); - } else if let Some(ref prob) = prob { - // Last probability could be left implicit - let lower_bound = Expression::NumComp { - op: NumCompOp::Leq, - left: Box::new(prob.clone()), - right: Box::new(rng.clone()), - }; - guard_exp = guard_exp - .map(|g| Expression::Bool { - op: BoolOp::And, - left: Box::new(lower_bound.clone()), - right: Box::new(g), - }) - .or(Some(lower_bound)); - // Need to remember this had a probability - dest.probability = Some(parser::Probability { - exp: Expression::IntOp { - op: parser::IntOp::Minus, - left: Box::new(Expression::ConstantValue( - parser::ConstantValue::NumberReal(1.), - )), - right: Box::new(prob.clone()), - }, - _comment: String::new(), - }); - } - - // actions need new unique names (tracking when new name is not necessary is difficult because of transient variables) - let action = edge_action.clone() + Self::GEN + &idx.to_string(); - idx += 1; - - new_edges.push(Edge { - location: edge.location.clone(), - action: Some(action.clone()), - guard: guard_exp.map(|exp| Guard { - exp, - _comment: String::new(), - }), - destinations: vec![dest.clone()], - _comment: String::new(), - }); - - // Update syncs with new action (has to synchronise like original one) - for e_idx in (0..jani_model.system.elements.len()).filter(|e_idx| { - jani_model.system.elements[*e_idx].automaton == automaton.name - }) { - // add new syncs for newly generated action - let to_add = jani_model - .system - .syncs - .iter() - .filter(|sync| { - sync.synchronise[e_idx] - .as_ref() - .is_some_and(|a| *a == edge_action) - }) - .map(|sync| { - let mut synchronise = sync.synchronise.clone(); - let _ = synchronise[e_idx].insert(action.clone()); - // Generate new unique result action - let result = sync.result.clone().unwrap_or_default() - + Self::GEN - + &idx.to_string(); - idx += 1; - Sync { - synchronise, - result: Some(result), - _comment: String::new(), - } - }) - .collect::>(); - jani_model.system.syncs.extend(to_add); - - // If original action did not appear in syncs it means that it does not sync between automata. - // We still want to keep track of it explicitly. - if jani_model.system.syncs.iter().all(|sync| { - sync.synchronise[e_idx] - .as_ref() - .is_none_or(|a| *a != edge_action) - }) { - let mut synchronise = vec![None; jani_model.system.elements.len()]; - synchronise[e_idx] = Some(action.clone()); - // ensure result is unique - let result = action.clone() + Self::GEN + &idx.to_string(); - idx += 1; - jani_model.system.syncs.push(Sync { - synchronise, - result: Some(result), - _comment: String::new(), - }); - } - } - } - } - // Keep only syncs that are actually used - jani_model.system.syncs.retain(|sync| { - jani_model - .system - .elements - .iter() - .enumerate() - .filter(|(_, e)| e.automaton == automaton.name) - .all(|(e_idx, _)| { - sync.synchronise[e_idx].as_ref().is_none_or(|a| { - new_edges - .iter() - .any(|edge| edge.action.as_ref().unwrap() == a) - }) - }) - }); - // Replace edges with new ones - automaton.edges = new_edges; - } - Ok(()) - } - - fn add_global_var( - &mut self, - pgb: &mut ProgramGraphBuilder, - var: &VariableDeclaration, - ) -> anyhow::Result<()> { - // TODO WARN FIXME: in JANI initial values are random? - let init = var - .initial_value - .as_ref() - .and_then(|expr| self.build_expression(expr, &HashMap::new(), None).ok()) - .unwrap_or_else(|| { - PgExpression::from(match &var.r#type { - parser::Type::Basic(basic_type) => match basic_type { - parser::BasicType::Bool => scan_core::Val::Boolean(false), - parser::BasicType::Int => scan_core::Val::Integer(0), - parser::BasicType::Real => scan_core::Val::Float(0f64), - }, - parser::Type::Bounded(_bounded_type) => todo!(), - parser::Type::Clock(_) => todo!(), - parser::Type::Continuous(_) => todo!(), - }) - }); - let val = init.eval_constant()?; - let t = val.r#type(); - let var_id = pgb.new_var(val)?; - self.global_vars.insert(var.name.clone(), (var_id, val, t)); - Ok(()) + // , global_vars, predicates); + let data = self.data(properties); + Ok((cs_model, oracle, data)) } fn add_global_constant(&mut self, c: &ConstantDeclaration) -> anyhow::Result<()> { // TODO WARN FIXME: in JANI initial values are random? + let c_type = (&c.r#type).try_into().expect("convert type"); let val = c .value .as_ref() .and_then(|expr| { - self.build_expression(expr, &HashMap::new(), None) + self.build_expression(expr, Some(c_type), &HashMap::new()) .and_then(|e| e.eval_constant().map_err(|err| anyhow!(err))) .ok() }) @@ -414,36 +726,26 @@ impl JaniBuilder { fn add_local_var( &self, - pgb: &mut ProgramGraphBuilder, + cs: &mut ChannelSystemBuilder, + pg_id: PgId, var: &VariableDeclaration, local_vars: &mut HashMap, ) -> anyhow::Result<()> { // TODO WARN FIXME: in JANI initial values are random? + let var_type = (&var.r#type).try_into().expect("convert type"); let init = var .initial_value .as_ref() - .and_then(|expr| self.build_expression(expr, local_vars, None).ok()) - // .ok_or_else(|| anyhow!("missing initial value"))?; - .unwrap_or_else(|| { - PgExpression::from(match &var.r#type { - parser::Type::Basic(basic_type) => match basic_type { - parser::BasicType::Bool => scan_core::Val::Boolean(false), - parser::BasicType::Int => scan_core::Val::Integer(0), - parser::BasicType::Real => scan_core::Val::Float(0f64), - }, - parser::Type::Bounded(_bounded_type) => todo!(), - parser::Type::Clock(_) => todo!(), - parser::Type::Continuous(_) => todo!(), - }) - }); + .and_then(|expr| self.build_expression(expr, Some(var_type), local_vars).ok()) + .unwrap_or_else(|| CsExpression::from(var_type.default_value())); let val = init.eval_constant()?; let t = val.r#type(); - let var_id = pgb.new_var(val)?; + let var_id = cs.new_var(pg_id, val)?; local_vars.insert(var.name.clone(), (var_id, val, t)); Ok(()) } - fn data(self, jani_model: Model) -> JaniModelData { + fn data(self, properties: Vec) -> JaniModelData { JaniModelData { actions: self .system_actions @@ -451,293 +753,48 @@ impl JaniBuilder { .map(|(name, action)| (action, name)) .collect::>(), ports: self - .global_vars + .global_state_vec .into_iter() - .map(|(name, (_, _, t))| (name, t)) - .collect(), - guarantees: jani_model - .properties - .into_iter() - .map(|prop| prop.name) - .collect(), - } - } - - fn build_automaton( - &mut self, - jani_model: &Model, - pgb: &mut ProgramGraphBuilder, - automaton: &Automaton, - e_idx: usize, - ) -> anyhow::Result<()> { - // Initialize RNG - let rng = pgb.new_var(Val::from(0.)).expect("new var"); - automaton - .edges - .iter() - .filter(|edge| edge.location.as_str() == Self::INITIAL) - .for_each(|edge| { - // For all edges starting from the unique initial locations, - // get the corresponding action and add RNG assignment as an effect. - let system_action = jani_model - .system - .syncs - .iter() - .find(|sync| { - sync.synchronise[e_idx] - .as_ref() - .is_some_and(|a| a == edge.action.as_ref().expect("init action")) - }) - .expect("sync") - .result - .as_ref() - .expect("no silent result"); - let init_action = *self.system_actions.get(system_action).expect("exist"); - pgb.add_effect( - init_action, - rng, - PgExpression::Float(FloatExpr::Rand(Box::new(( - FloatExpr::from(0.), - FloatExpr::from(1.), - )))), - ) - .expect("add effect"); - }); - - // Add locations - let mut locations: HashMap = HashMap::new(); - for location in &automaton.locations { - self.build_location(jani_model, pgb, location, e_idx, &mut locations) - .with_context(|| format!("failed building location: {}", &location.name))?; - } - - // Add local variables - let mut local_vars: HashMap = HashMap::new(); - automaton - .variables - .iter() - .try_for_each(|var| self.add_local_var(pgb, var, &mut local_vars)) - .context("failed adding local variables")?; - - // Add edges - let mut rng_actions = HashSet::new(); - for (n_edge, edge) in automaton.edges.iter().enumerate() { - self.build_edge( - jani_model, - automaton, - pgb, - edge, - e_idx, - &local_vars, - &locations, - &mut rng_actions, - rng, - ) - .with_context(|| { - format!( - "failed building {}-th edge for action {}", - n_edge + 1, - edge.action.clone().unwrap_or(String::from("silent")) - ) - })?; - } - Ok(()) - } - - fn build_location( - &mut self, - jani_model: &Model, - pgb: &mut ProgramGraphBuilder, - location: &Location, - e_idx: usize, - locations: &mut HashMap, - ) -> anyhow::Result<()> { - let loc = pgb.new_location(); - // Initial location has to be the start of the new process - if location.name.as_str() == Self::INITIAL { - pgb.new_process(loc).expect("new process"); - } - assert!(locations.insert(location.name.clone(), loc).is_none()); - // For every action that is **NOT** synchronised on this automaton, - // allow action with no change in state. - jani_model - .system - .syncs - .iter() - .filter(|sync| sync.synchronise[e_idx].is_none()) - .for_each(|sync| { - let result = sync.result.as_ref().expect("result must have name"); - let action = self.system_actions.get(result).expect("system action"); - pgb.add_transition(loc, *action, loc, None).unwrap(); - }); - Ok(()) - } - - fn build_edge( - &mut self, - jani_model: &Model, - automaton: &Automaton, - pgb: &mut ProgramGraphBuilder, - edge: &Edge, - e_idx: usize, - local_vars: &HashMap, - locations: &HashMap, - rng_actions: &mut HashSet, - rng: Var, - ) -> anyhow::Result<()> { - let pre = locations.get(&edge.location).ok_or(anyhow!( - "pre-transition location {} not found", - edge.location - ))?; - let guard = edge - .guard - .as_ref() - .map(|guard| self.build_expression(&guard.exp, local_vars, Some(rng))) - .transpose() - .with_context(|| { - format!( - "failed to build guard with expression {:?}", - edge.guard.as_ref().map(|g| &g.exp) - ) - })?; - let guard = guard - .map(|guard| { - if let PgExpression::Boolean(bool_expr) = guard { - Ok(bool_expr) - } else { - bail!("guard is not a boolean expression") - } - }) - .transpose()?; - // There must be only one destination per edge! - if let [dest] = edge.destinations.as_slice() { - let post = locations.get(&dest.location).ok_or(anyhow!( - "post-transition location {} not found", - dest.location - ))?; - jani_model - .system - .syncs - .iter() - .filter(|sync| { - sync.synchronise[e_idx].as_ref().is_some_and(|sync_action| { - *edge.action.as_ref().expect("no silent action") == *sync_action - }) + .map(|name| { + self.global_vars + .get(&name) + .map(|(_var, _, t)| (name, *t)) + .unwrap() }) - .try_for_each(|sync| { - let result = sync.result.as_ref().expect("no silent actions generated"); - let action = self.system_actions.get(result).unwrap(); - // checks to do this only once per action - if dest.probability.is_some() && !rng_actions.contains(action) { - pgb.add_effect( - *action, - rng, - PgExpression::Float(FloatExpr::Rand(Box::new(( - FloatExpr::from(0.), - FloatExpr::from(1.), - )))), - ) - .expect("effect"); - rng_actions.insert(*action); - } - // Set transient variables' values as their initial values before transition from pre location - for transient_value in automaton - .locations - .iter() - .find(|loc| loc.name == edge.location) - .map(|loc| &loc.transient_values) - .ok_or(anyhow!( - "post-transition location {} not found", - edge.location - ))? - { - let r#ref = &transient_value.r#ref; - let (var, val, _) = local_vars - .get(r#ref) - .or_else(|| self.global_vars.get(r#ref)) - .ok_or(anyhow!("variable {} not found", r#ref))?; - let expr = scan_core::Expression::from(*val); - pgb.add_effect(*action, *var, expr).context( - "failed setting transient variable {r#ref} to initial value", - )?; - } - // Apply assignments - for (n, assignment) in dest.assignments.iter().enumerate() { - let (var, ..) = local_vars - .get(&assignment.r#ref) - .or_else(|| self.global_vars.get(&assignment.r#ref)) - .ok_or_else(|| anyhow!("unknown id `{}`", &assignment.r#ref))?; - let expr = self - .build_expression(&assignment.value, local_vars, Some(rng)) - .context("failed building expression")?; - pgb.add_effect(*action, *var, expr).with_context(|| { - format!("failed adding {}-th assignment to action", n + 1) - })?; - } - // Set transient variables' values for destination location - for transient_value in automaton - .locations - .iter() - .find(|loc| loc.name == dest.location) - .map(|loc| &loc.transient_values) - .ok_or(anyhow!( - "post-transition location {} not found", - dest.location - ))? - { - let r#ref = &transient_value.r#ref; - let (var, ..) = local_vars - .get(r#ref) - .or_else(|| self.global_vars.get(r#ref)) - .ok_or(anyhow!("variable {} not found", r#ref))?; - let expr = - self.build_expression(&transient_value.value, local_vars, Some(rng))?; - pgb.add_effect(*action, *var, expr).context( - "failed setting transient variable {r#ref} to transient value", - )?; - } - pgb.add_transition(*pre, *action, *post, guard.clone()) - .context("failed adding transition") - })?; - } else { - panic!("edges should be normalized"); + .collect(), + guarantees: properties, } - Ok(()) } fn build_expression( &self, expr: &Expression, + type_hint: Option, local_vars: &HashMap, - rng: Option, - ) -> anyhow::Result { + ) -> anyhow::Result { match expr { Expression::ConstantValue(constant_value) => match constant_value { - parser::ConstantValue::Boolean(b) => Ok(PgExpression::from(*b)), + parser::ConstantValue::Boolean(b) => Ok(CsExpression::from(*b)), parser::ConstantValue::Constant(constant) => match constant { - parser::Constant::Euler => Ok(PgExpression::from(std::f64::consts::E)), - parser::Constant::Pi => Ok(PgExpression::from(std::f64::consts::PI)), + parser::Constant::Euler => Ok(CsExpression::from(std::f64::consts::E)), + parser::Constant::Pi => Ok(CsExpression::from(std::f64::consts::PI)), + }, + parser::ConstantValue::NumberReal(num) => Ok(CsExpression::from(*num)), + parser::ConstantValue::NumberInt(num) => match type_hint { + Some(Type::Float) => Ok(CsExpression::from(*num as Float)), + Some(Type::Natural) => Ok(CsExpression::from(*num as Natural)), + _ => Ok(CsExpression::from(*num as Integer)), }, - parser::ConstantValue::NumberReal(num) => Ok(PgExpression::from(*num)), - parser::ConstantValue::NumberInt(num) => Ok(PgExpression::from(*num)), }, - Expression::Identifier(id) if id == Self::RNG => rng - .ok_or_else(|| anyhow!("rng not available")) - .map(|rng| PgExpression::Float(FloatExpr::Var(rng))), Expression::Identifier(id) => local_vars .get(id) .or_else(|| self.global_vars.get(id)) - .map(|(var, _, t)| match t { - Type::Boolean => PgExpression::Boolean(scan_core::BooleanExpr::Var(*var)), - Type::Natural => PgExpression::Natural(scan_core::NaturalExpr::Var(*var)), - Type::Integer => PgExpression::Integer(scan_core::IntegerExpr::Var(*var)), - Type::Float => PgExpression::Float(scan_core::FloatExpr::Var(*var)), - }) + .map(|(var, _, t)| CsExpression::from_var(*var, *t)) .or_else(|| { self.global_constants .get(id) .cloned() - .map(PgExpression::from) + .map(CsExpression::from) }) .ok_or_else(|| anyhow!("unknown id `{id}`")), Expression::IfThenElse { @@ -746,20 +803,20 @@ impl JaniBuilder { then, r#else, } => { - let r#if = self.build_expression(r#if, local_vars, rng)?; - let then = self.build_expression(then, local_vars, rng)?; - let r#else = self.build_expression(r#else, local_vars, rng)?; + let r#if = self.build_expression(r#if, Some(Type::Boolean), local_vars)?; + let then = self.build_expression(then, type_hint, local_vars)?; + let r#else = self.build_expression(r#else, type_hint, local_vars)?; match op { parser::IteOp::Ite => r#if.ite(then, r#else).map_err(anyhow::Error::from), } } Expression::Bool { op, left, right } => { - let left = self.build_expression(left, local_vars, rng)?; - let right = self.build_expression(right, local_vars, rng)?; + let left = self.build_expression(left, Some(Type::Boolean), local_vars)?; + let right = self.build_expression(right, Some(Type::Boolean), local_vars)?; match op { BoolOp::And => left & right, BoolOp::Or => left | right, - BoolOp::Implies => Ok(PgExpression::Boolean(BooleanExpr::Implies(Box::new(( + BoolOp::Implies => Ok(CsExpression::Boolean(BooleanExpr::Implies(Box::new(( BooleanExpr::try_from(left)?, BooleanExpr::try_from(right)?, ))))), @@ -767,48 +824,63 @@ impl JaniBuilder { .map_err(anyhow::Error::from) } Expression::Neg { op, exp } => { - let exp = self.build_expression(exp, local_vars, rng)?; + let exp = self.build_expression(exp, Some(Type::Boolean), local_vars)?; match op { - parser::NegOp::Neg => PgExpression::not(exp).map_err(|err| err.into()), + parser::NegOp::Neg => (!exp).map_err(|err| err.into()), } } Expression::EqComp { op, left, right } => { - let left = self.build_expression(left, local_vars, rng)?; - let right = self.build_expression(right, local_vars, rng)?; + let left = self.build_expression(left, None, local_vars)?; + let right = self.build_expression(right, None, local_vars)?; match op { - parser::EqCompOp::Eq => PgExpression::equal_to(left, right), - parser::EqCompOp::Neq => PgExpression::equal_to(left, right).map(|expr| !expr), + parser::EqCompOp::Eq => CsExpression::equal_to(left, right), + parser::EqCompOp::Neq => CsExpression::equal_to(left, right).map(|expr| !expr), } - .map(PgExpression::Boolean) + .map(CsExpression::Boolean) .map_err(anyhow::Error::from) } Expression::NumComp { op, left, right } => { - let left = self.build_expression(left, local_vars, rng)?; - let right = self.build_expression(right, local_vars, rng)?; + let left = self.build_expression(left, None, local_vars)?; + let right = self.build_expression(right, None, local_vars)?; match op { - parser::NumCompOp::Less => PgExpression::less_than(left, right), - parser::NumCompOp::Leq => PgExpression::less_than_or_equal_to(left, right), - parser::NumCompOp::Greater => PgExpression::greater_than(left, right), - parser::NumCompOp::Geq => PgExpression::greater_than_or_equal_to(left, right), + parser::NumCompOp::Less => CsExpression::less_than(left, right), + parser::NumCompOp::Leq => CsExpression::less_than_or_equal_to(left, right), + parser::NumCompOp::Greater => CsExpression::greater_than(left, right), + parser::NumCompOp::Geq => CsExpression::greater_than_or_equal_to(left, right), } - .map(PgExpression::Boolean) + .map(CsExpression::Boolean) .map_err(anyhow::Error::from) } Expression::IntOp { op, left, right } => { - let left = self.build_expression(left, local_vars, rng)?; - let right = self.build_expression(right, local_vars, rng)?; + let left = self.build_expression(left, type_hint, local_vars)?; + let right = self.build_expression(right, type_hint, local_vars)?; match op { parser::IntOp::Plus => left + right, parser::IntOp::Minus => left + (-right)?, parser::IntOp::Mult => left * right, - parser::IntOp::IntDiv => left / right, + parser::IntOp::Mod + if type_hint.is_some_and(|hint| matches!(hint, Type::Natural)) => + { + let left = NaturalExpr::try_from(left)?; + let right = NaturalExpr::try_from(right)?; + Ok(CsExpression::Natural(NaturalExpr::Rem(Box::new(( + left, right, + ))))) + } + parser::IntOp::Mod => { + let left = IntegerExpr::try_from(left)?; + let right = IntegerExpr::try_from(right)?; + Ok(CsExpression::Integer(IntegerExpr::Rem(Box::new(( + left, right, + ))))) + } } .map_err(anyhow::Error::from) } Expression::RealOp { op, left, right } => { - let left = self.build_expression(left, local_vars, rng)?; - let right = self.build_expression(right, local_vars, rng)?; + let left = self.build_expression(left, Some(Type::Float), local_vars)?; + let right = self.build_expression(right, Some(Type::Float), local_vars)?; match op { parser::RealOp::Div => left / right, parser::RealOp::Pow => todo!(), @@ -817,12 +889,14 @@ impl JaniBuilder { .map_err(anyhow::Error::from) } Expression::Real2IntOp { op, exp } => { - let _exp = self.build_expression(exp, local_vars, rng)?; - if matches!(_exp.r#type(), Type::Float) { - match op { - parser::Real2IntOp::Floor => todo!(), - parser::Real2IntOp::Ceil => todo!(), - } + let exp = self.build_expression(exp, None, local_vars)?; + if matches!(exp.r#type(), Type::Float) { + Ok(CsExpression::Integer(match op { + parser::Real2IntOp::Floor => IntegerExpr::Floor, + parser::Real2IntOp::Ceil => IntegerExpr::Ceil, + }(Box::new( + FloatExpr::try_from(exp)?, + )))) } else { bail!(TypeError::TypeMismatch) } @@ -833,36 +907,42 @@ impl JaniBuilder { fn build_property( &self, prop: &PropertyExpression, - ) -> anyhow::Result>> { + ) -> anyhow::Result, Mtl>>> + { + use scan_core::Expression; match prop { PropertyExpression::ConstantValue(constant_value) => { Ok(Either::Left(match constant_value { - parser::ConstantValue::Boolean(b) => PgExpression::from(*b), + parser::ConstantValue::Boolean(b) => Expression::from(*b), parser::ConstantValue::Constant(constant) => match constant { - parser::Constant::Euler => PgExpression::from(std::f64::consts::E), - parser::Constant::Pi => PgExpression::from(std::f64::consts::PI), + parser::Constant::Euler => Expression::from(std::f64::consts::E), + parser::Constant::Pi => Expression::from(std::f64::consts::PI), }, - parser::ConstantValue::NumberReal(num) => PgExpression::from(*num), - parser::ConstantValue::NumberInt(num) => PgExpression::from(*num), + parser::ConstantValue::NumberReal(num) => Expression::from(*num), + parser::ConstantValue::NumberInt(num) => Expression::from(*num), })) } - PropertyExpression::Identifier(id) => self - .global_vars - .get(id) - .map(|(var, _, t)| match t { - Type::Boolean => PgExpression::Boolean(scan_core::BooleanExpr::Var(*var)), - Type::Natural => PgExpression::Natural(scan_core::NaturalExpr::Var(*var)), - Type::Integer => PgExpression::Integer(scan_core::IntegerExpr::Var(*var)), - Type::Float => PgExpression::Float(scan_core::FloatExpr::Var(*var)), - }) - .or_else(|| { - self.global_constants - .get(id) - .cloned() - .map(PgExpression::from) - }) - .map(Either::Left) - .ok_or_else(|| anyhow!("unknown id `{id}`")), + PropertyExpression::Identifier(id) => { + if let Some((_, _, t)) = self.global_vars.get(id) { + let var_idx = self + .global_state_vec + .iter() + .position(|name| name == id) + .ok_or_else(|| anyhow!("var not a system var"))?; + let atom = Atom::State( + self.global_state_channel.expect("global state channel"), + var_idx, + ); + let expr = Expression::from_var(atom, *t); + Ok(Either::Left(expr)) + } else if let Some(constant) = + self.global_constants.get(id).cloned().map(Expression::from) + { + Ok(Either::Left(constant)) + } else { + Err(anyhow!("unknown identifier")) + } + } PropertyExpression::IfThenElse { op, r#if, @@ -884,7 +964,7 @@ impl JaniBuilder { match op { BoolOp::And => left & right, BoolOp::Or => left | right, - BoolOp::Implies => Ok(PgExpression::Boolean(BooleanExpr::Implies(Box::new(( + BoolOp::Implies => Ok(Expression::Boolean(BooleanExpr::Implies(Box::new(( BooleanExpr::try_from(left)?, BooleanExpr::try_from(right)?, ))))), @@ -895,7 +975,7 @@ impl JaniBuilder { PropertyExpression::Neg { op, exp } => { let exp = self.build_property(exp)?.left().expect("expression"); match op { - parser::NegOp::Neg => PgExpression::not(exp).map_err(|err| err.into()), + parser::NegOp::Neg => (!exp).map_err(|err| err.into()), } .map(Either::Left) } @@ -907,12 +987,12 @@ impl JaniBuilder { && matches!(right.r#type(), Type::Integer | Type::Float)) { match op { - parser::EqCompOp::Eq => PgExpression::equal_to(left, right), + parser::EqCompOp::Eq => Expression::equal_to(left, right), parser::EqCompOp::Neq => { - PgExpression::equal_to(left, right).map(|expr| !expr) + Expression::equal_to(left, right).map(|expr| !expr) } } - .map(PgExpression::Boolean) + .map(Expression::Boolean) .map(Either::Left) .map_err(anyhow::Error::from) } else { @@ -923,12 +1003,12 @@ impl JaniBuilder { let left = self.build_property(left)?.left().expect("expression"); let right = self.build_property(right)?.left().expect("expression"); match op { - parser::NumCompOp::Less => PgExpression::less_than(left, right), - parser::NumCompOp::Leq => PgExpression::less_than_or_equal_to(left, right), - parser::NumCompOp::Greater => PgExpression::greater_than(left, right), - parser::NumCompOp::Geq => PgExpression::greater_than_or_equal_to(left, right), + parser::NumCompOp::Less => Expression::less_than(left, right), + parser::NumCompOp::Leq => Expression::less_than_or_equal_to(left, right), + parser::NumCompOp::Greater => Expression::greater_than(left, right), + parser::NumCompOp::Geq => Expression::greater_than_or_equal_to(left, right), } - .map(PgExpression::Boolean) + .map(Expression::Boolean) .map(Either::Left) .map_err(anyhow::Error::from) } @@ -939,7 +1019,7 @@ impl JaniBuilder { parser::IntOp::Plus => left + right, parser::IntOp::Minus => left + (-right)?, parser::IntOp::Mult => left * right, - parser::IntOp::IntDiv => left / right, + parser::IntOp::Mod => left / right, } .map(Either::Left) .map_err(anyhow::Error::from) @@ -966,10 +1046,20 @@ impl JaniBuilder { .build_property(left)? .left() .ok_or(anyhow!("unsupported property"))?; + let left = if let scan_core::Expression::Boolean(expr) = left { + expr + } else { + bail!("not a boolean expression") + }; let right = self .build_property(right)? .left() .ok_or(anyhow!("unsupported property"))?; + let right = if let scan_core::Expression::Boolean(expr) = right { + expr + } else { + bail!("not a boolean expression") + }; Ok(Either::Right(match op { parser::UntilOp::Until => Mtl::Until(left, right), parser::UntilOp::WeakUntil => todo!(), diff --git a/scan_jani/src/lib.rs b/scan_jani/src/lib.rs index 46baa2e..f31d5af 100644 --- a/scan_jani/src/lib.rs +++ b/scan_jani/src/lib.rs @@ -9,12 +9,12 @@ pub use builder::JaniModelData; use builder::build; use log::info; use parser::Model; -use scan_core::PgModel; -use scan_core::{MtlOracle, Scan}; +use scan_core::Scan; +use scan_mtl::MtlOracle; use std::{fs::File, io::Read, path::Path}; pub use tracer::TracePrinter; -pub type JaniScan = Scan; +pub type JaniScan = Scan; pub fn load<'def>( path: &'def Path, diff --git a/scan_jani/src/parser.rs b/scan_jani/src/parser.rs index 247a06a..3cd29db 100644 --- a/scan_jani/src/parser.rs +++ b/scan_jani/src/parser.rs @@ -71,7 +71,7 @@ pub(crate) struct Action { pub(crate) name: Identifier, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: (), } #[derive(Deserialize)] @@ -138,5 +138,5 @@ pub(crate) struct RestrictInitial { pub(crate) exp: Expression, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: (), } diff --git a/scan_jani/src/parser/automaton.rs b/scan_jani/src/parser/automaton.rs index a1e351a..e3f88fe 100644 --- a/scan_jani/src/parser/automaton.rs +++ b/scan_jani/src/parser/automaton.rs @@ -1,5 +1,5 @@ use super::{Expression, Identifier, LValue, RestrictInitial, VariableDeclaration}; -use serde::Deserialize; +use serde::{Deserialize, de::IgnoredAny}; /// all expressions and assignments inside an automaton can only reference its own local /// variables and the global variables of the enclosing model @@ -24,7 +24,7 @@ pub(crate) struct Automaton { pub(crate) edges: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Deserialize)] @@ -38,7 +38,7 @@ pub(crate) struct Location { pub(crate) transient_values: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, // TODO // "?time-progress": { // the location's time progress condition, not allowed except TA, PTA, STA, HA, PHA and STA, // // type bool; if omitted in TA, PTA, STA, HA, PHA or SHA, it is true @@ -58,7 +58,7 @@ pub(crate) struct TransientValue { pub(crate) value: Expression, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Clone, Deserialize)] @@ -82,7 +82,7 @@ pub(crate) struct Edge { pub(crate) destinations: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Clone, Deserialize)] @@ -92,7 +92,7 @@ pub(crate) struct Guard { pub(crate) exp: Expression, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Clone, Deserialize)] @@ -108,7 +108,7 @@ pub(crate) struct Destination { pub(crate) assignments: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Clone, Deserialize)] @@ -123,7 +123,7 @@ pub(crate) struct Assignment { // "?index": Number.step(1), // the index, to create sequences of atomic assignment sets, default 0 /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Clone, Deserialize)] @@ -133,5 +133,5 @@ pub(crate) struct Probability { pub(crate) exp: Expression, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } diff --git a/scan_jani/src/parser/composition.rs b/scan_jani/src/parser/composition.rs index b0895d5..8845827 100644 --- a/scan_jani/src/parser/composition.rs +++ b/scan_jani/src/parser/composition.rs @@ -1,5 +1,5 @@ use super::Identifier; -use serde::Deserialize; +use serde::{Deserialize, de::IgnoredAny}; /// Automata composition #[derive(Deserialize)] @@ -10,7 +10,7 @@ pub(crate) struct Composition { pub(crate) syncs: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Deserialize)] @@ -25,7 +25,7 @@ pub(crate) struct Element { pub(crate) input_enable: Vec, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Deserialize)] @@ -38,5 +38,5 @@ pub(crate) struct Sync { pub(crate) result: Option, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } diff --git a/scan_jani/src/parser/constant_declaration.rs b/scan_jani/src/parser/constant_declaration.rs index f82ce91..34f9819 100644 --- a/scan_jani/src/parser/constant_declaration.rs +++ b/scan_jani/src/parser/constant_declaration.rs @@ -1,5 +1,5 @@ use super::{Expression, Identifier, Type}; -use serde::Deserialize; +use serde::{Deserialize, de::IgnoredAny}; #[derive(Deserialize)] #[allow(dead_code)] @@ -17,5 +17,5 @@ pub(crate) struct ConstantDeclaration { pub(crate) value: Option, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } diff --git a/scan_jani/src/parser/expression.rs b/scan_jani/src/parser/expression.rs index a1d2adf..b286e77 100644 --- a/scan_jani/src/parser/expression.rs +++ b/scan_jani/src/parser/expression.rs @@ -168,7 +168,7 @@ pub(crate) enum IntOp { #[serde(rename = "*")] Mult, #[serde(rename = "%")] - IntDiv, + Mod, } /// computes left + right / left - right / left * right / left modulo right diff --git a/scan_jani/src/parser/jani_type.rs b/scan_jani/src/parser/jani_type.rs index d7d5ae5..a3430d9 100644 --- a/scan_jani/src/parser/jani_type.rs +++ b/scan_jani/src/parser/jani_type.rs @@ -5,7 +5,7 @@ use serde::Deserialize; /// We cover only the most basic types at the moment. /// In the remainder of the specification, all requirements like "y must be of type x" are to be interpreted /// as "type x must be assignable from y's type". -#[derive(Deserialize)] +#[derive(Debug, Clone, Copy, Deserialize)] #[serde(rename_all = "kebab-case")] pub(crate) enum BasicType { /// assignable from bool @@ -16,6 +16,16 @@ pub(crate) enum BasicType { Real, } +impl From for scan_core::Type { + fn from(val: BasicType) -> Self { + match val { + BasicType::Bool => scan_core::Type::Boolean, + BasicType::Int => scan_core::Type::Integer, + BasicType::Real => scan_core::Type::Float, + } + } +} + #[derive(Deserialize, Default)] #[serde(rename_all = "kebab-case")] pub(crate) enum BoundedTypeKind { @@ -52,3 +62,16 @@ pub(crate) enum Type { /// invariant; only allowed for HA, PHA and SHA; assignable from all numeric types Continuous(f64), } + +impl TryInto for &Type { + type Error = (); + + fn try_into(self) -> Result { + match self { + Type::Basic(basic_type) => Ok((*basic_type).into()), + Type::Bounded(bounded_type) => Ok(bounded_type.base.into()), + Type::Clock(_) => todo!(), + Type::Continuous(_) => todo!(), + } + } +} diff --git a/scan_jani/src/parser/property.rs b/scan_jani/src/parser/property.rs index fcef6bd..a33902f 100644 --- a/scan_jani/src/parser/property.rs +++ b/scan_jani/src/parser/property.rs @@ -2,7 +2,7 @@ use super::{ BoolOp, ConstantValue, EqCompOp, Expression, Identifier, IntOp, IteOp, NegOp, NumCompOp, Real2IntOp, RealOp, }; -use serde::Deserialize; +use serde::{Deserialize, de::IgnoredAny}; #[derive(Deserialize)] #[serde(deny_unknown_fields, rename_all = "kebab-case")] @@ -13,7 +13,7 @@ pub(crate) struct Property { pub(crate) expression: PropertyExpression, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } #[derive(Deserialize)] diff --git a/scan_jani/src/parser/variable_declaration.rs b/scan_jani/src/parser/variable_declaration.rs index dea10cf..0a1e5ac 100644 --- a/scan_jani/src/parser/variable_declaration.rs +++ b/scan_jani/src/parser/variable_declaration.rs @@ -1,5 +1,5 @@ use super::{Expression, Identifier, Type}; -use serde::Deserialize; +use serde::{Deserialize, de::IgnoredAny}; #[derive(Deserialize)] #[allow(dead_code)] @@ -25,5 +25,5 @@ pub(crate) struct VariableDeclaration { pub(crate) initial_value: Option, /// an optional comment #[serde(skip)] - pub(crate) _comment: String, + pub(crate) _comment: IgnoredAny, } diff --git a/scan_jani/src/tracer.rs b/scan_jani/src/tracer.rs index 9fb5bcf..c38dcff 100644 --- a/scan_jani/src/tracer.rs +++ b/scan_jani/src/tracer.rs @@ -1,148 +1,61 @@ use super::JaniModelData; -use scan_core::{RunOutcome, Time, Tracer, Val, program_graph::Action}; -use std::{ - env::current_dir, - fs::{File, create_dir, create_dir_all, exists, remove_file, rename}, - path::PathBuf, - sync::{Arc, atomic::AtomicU32}, +use scan_core::{ + Time, TraceWriter, Tracer, Val, + channel_system::{Action, Event}, }; pub struct TracePrinter { - index: Arc, - path: PathBuf, - writer: Option>>, - model: Arc, + writer: csv::Writer, } impl TracePrinter { - const FOLDER: &str = "traces"; - const TEMP: &str = ".temp"; - const SUCCESSES: &str = "successes"; - const FAILURES: &str = "failures"; - const HEADER: [&str; 2] = ["Time", "Action"]; - - pub fn new(model: Arc) -> Self { - let mut path = current_dir().expect("current dir"); - for i in 0.. { - path.push(format!("{}_{i:02}", Self::FOLDER)); - if std::fs::create_dir(&path).is_ok() { - path.push(Self::TEMP); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - path.push(Self::SUCCESSES); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - path.push(Self::FAILURES); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - break; - } else { - assert!(path.pop()); - } - } - - Self { - index: Arc::new(AtomicU32::new(0)), - path, - writer: None, - model, - } - } + const HEADER: [&'static str; 2] = ["Time", "Action"]; + const UNKNOWN_ACTION: &'static str = "unknown action"; } -impl Clone for TracePrinter { - fn clone(&self) -> Self { - // Get the temp folder - let mut path = self.path.clone(); - if path.is_file() { - path.pop(); - } - Self { - index: Arc::clone(&self.index), - path, - writer: None, - model: Arc::clone(&self.model), - } - } -} +impl Tracer for TracePrinter { + const EXTENSION: &'static str = "csv"; + + type ModelData = JaniModelData; -impl Tracer for TracePrinter { - fn init(&mut self) { - let idx = self - .index - .fetch_add(1, std::sync::atomic::Ordering::Relaxed); - let filename = format!("{idx:04}.csv.gz"); - self.path.push(Self::TEMP); - self.path.push(&filename); - let file = File::create_new(&self.path).expect("create file"); - let enc = flate2::GzBuilder::new() - .filename(filename) - .write(file, flate2::Compression::fast()); - let mut writer = csv::WriterBuilder::new().from_writer(enc); + fn init(writer: TraceWriter, data: &Self::ModelData) -> Self { + let mut writer = csv::Writer::from_writer(writer); writer .write_record( - Self::HEADER.into_iter().map(String::from).chain( - self.model - .ports - .iter() - .map(|(name, t)| format!("{name}: {t:?}")), - ), + Self::HEADER + .into_iter() + .map(String::from) + .chain(data.ports.iter().map(|(name, t)| format!("{name}: {t:?}"))), ) .expect("write header"); - self.writer = Some(writer); + + Self { writer } } - fn trace>(&mut self, action: &Action, time: Time, ports: I) { + fn trace( + &mut self, + data: &Self::ModelData, + action: Action, + _event: &Event, + time: Time, + ports: &[Vec], + ) { let time = time.to_string(); - let action_name = self.model.actions.get(action).cloned().unwrap_or_default(); + let action_name = data + .actions + .get(&action) + .cloned() + .unwrap_or(Self::UNKNOWN_ACTION.to_string()); + // self.model.actions.get(event).cloned().unwrap_or_default(); self.writer - .as_mut() - .unwrap() .write_record( [time, action_name] .into_iter() - .chain(ports.into_iter().map(format_val)), + .chain(ports.first().unwrap().iter().copied().map(format_val)), ) .expect("write record"); } - - fn finalize(self, outcome: &RunOutcome) { - let mut writer = self.writer.unwrap(); - writer.flush().expect("flush csv content"); - writer - .into_inner() - .expect("encoder") - .try_finish() - .expect("finish"); - - let mut new_path = self.path.clone(); - // pop file name - new_path.pop(); - // pop temp folder - new_path.pop(); - match outcome { - RunOutcome::Verified(verified) => { - if verified.iter().all(|b| *b) { - new_path.push(Self::SUCCESSES); - } else { - new_path.push(Self::FAILURES); - // new_path.push(self.model.guarantees.get(violation).unwrap()); - // This path might not exist yet - if !exists(new_path.as_path()).expect("check folder") { - create_dir_all(new_path.clone()).expect("create missing folder"); - } - } - } - RunOutcome::Incomplete => { - remove_file(&self.path).expect("delete file"); - return; - } - } - - new_path.push(self.path.file_name().expect("file name")); - rename(&self.path, new_path).expect("renaming"); - } } fn format_val(val: Val) -> String { diff --git a/scan_mtl/Cargo.toml b/scan_mtl/Cargo.toml new file mode 100644 index 0000000..7af0982 --- /dev/null +++ b/scan_mtl/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "smc_scan_mtl" +version = "0.1.0" +edition = "2024" +description = "MTL oracle for the Scan model checker." +documentation = "https://convince-project.github.io/scan/crates/scan_mtl/index.html" +homepage = "https://convince-project.github.io/scan/" +repository = "https://github.com/convince-project/scan" +license = "Apache-2.0" +readme = "README.md" +keywords = ["verification", "model-checking", "mtl"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] + +[lib] +name = "scan_mtl" # The name of the target. +crate-type = ["lib"] # The crate types to generate. + +[dependencies] +smc_scan_core = { version = "0.2.0", path = "../scan_core" } diff --git a/scan_mtl/src/lib.rs b/scan_mtl/src/lib.rs new file mode 100644 index 0000000..270e7d3 --- /dev/null +++ b/scan_mtl/src/lib.rs @@ -0,0 +1,3 @@ +mod oracle; + +pub use oracle::{Mtl, MtlOracle}; diff --git a/scan_core/src/oracle/mtl.rs b/scan_mtl/src/oracle.rs similarity index 98% rename from scan_core/src/oracle/mtl.rs rename to scan_mtl/src/oracle.rs index 1d5de67..55633a3 100644 --- a/scan_core/src/oracle/mtl.rs +++ b/scan_mtl/src/oracle.rs @@ -1,4 +1,4 @@ -use crate::{Oracle, Time}; +use scan_core::{Oracle, Time}; /// An Metric Temporal Logic (MTL) formula. #[derive(Debug, Clone)] diff --git a/scan_pmtl/Cargo.toml b/scan_pmtl/Cargo.toml new file mode 100644 index 0000000..2c6bdfe --- /dev/null +++ b/scan_pmtl/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "smc_scan_pmtl" +version = "0.1.0" +edition = "2024" +description = "pMTL oracle for the Scan model checker." +documentation = "https://convince-project.github.io/scan/crates/scan_pmtl/index.html" +homepage = "https://convince-project.github.io/scan/" +repository = "https://github.com/convince-project/scan" +license = "Apache-2.0" +readme = "README.md" +keywords = ["verification", "model-checking", "pmtl"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] + +[lib] +name = "scan_pmtl" # The name of the target. +crate-type = ["lib"] # The crate types to generate. + +[dependencies] +smc_scan_core = { version = "0.2.0", path = "../scan_core" } diff --git a/scan_pmtl/src/lib.rs b/scan_pmtl/src/lib.rs new file mode 100644 index 0000000..3ab2ca3 --- /dev/null +++ b/scan_pmtl/src/lib.rs @@ -0,0 +1,3 @@ +mod oracle; + +pub use oracle::{Pmtl, PmtlOracle}; diff --git a/scan_core/src/oracle/pmtl.rs b/scan_pmtl/src/oracle.rs similarity index 99% rename from scan_core/src/oracle/pmtl.rs rename to scan_pmtl/src/oracle.rs index dac7797..c32905e 100644 --- a/scan_core/src/oracle/pmtl.rs +++ b/scan_pmtl/src/oracle.rs @@ -1,7 +1,7 @@ mod numset; -use crate::{Oracle, Time}; use numset::NumSet; +use scan_core::{Oracle, Time}; use std::hash::Hash; /// A Past-time Metric Temporal Logic (PMTL) formula. @@ -76,7 +76,6 @@ impl From<&Pmtl> for ValPmtl { impl ValPmtl { // From Ulus 2024: Online monitoring of metric temporal logic using sequential networks. Link: - #[inline(always)] pub fn output(&self, time: Time) -> bool { match self { ValPmtl::True => true, @@ -304,18 +303,22 @@ impl PmtlOracle { } impl Oracle for PmtlOracle { + #[inline] fn output_assumes(&self) -> impl Iterator> { self.assumes.iter().map(|f| f.valuation(self.time)) } + #[inline] fn output_guarantees(&self) -> impl Iterator> { self.guarantees.iter().map(|f| f.valuation(self.time)) } + #[inline] fn final_output_assumes(&self) -> impl Iterator { self.assumes.iter().map(|f| f.output(self.time)) } + #[inline] fn final_output_guarantees(&self) -> impl Iterator { self.guarantees.iter().map(|f| f.output(self.time)) } diff --git a/scan_core/src/oracle/pmtl/numset.rs b/scan_pmtl/src/oracle/numset.rs similarity index 97% rename from scan_core/src/oracle/pmtl/numset.rs rename to scan_pmtl/src/oracle/numset.rs index 853675c..866c226 100644 --- a/scan_core/src/oracle/pmtl/numset.rs +++ b/scan_pmtl/src/oracle/numset.rs @@ -1,4 +1,4 @@ -use crate::Time; +use scan_core::Time; // Represent union of closed intervals, // each interval being represented by lower and upper bounds. @@ -8,23 +8,23 @@ use crate::Time; pub(super) struct NumSet(Vec<(Time, Time)>); impl NumSet { - #[inline(always)] + #[inline] pub(super) fn empty() -> Self { Self(Vec::new()) } - #[inline(always)] + #[inline] fn _full() -> Self { Self(vec![(0, Time::MAX)]) } - #[inline(always)] + #[inline] pub(super) fn from_range(lower_bound: Time, upper_bound: Time) -> Self { assert!(lower_bound <= upper_bound); Self(vec![(lower_bound, upper_bound)]) } - #[inline(always)] + #[inline] pub(super) fn contains(&self, t: Time) -> bool { match self.0.binary_search_by_key(&t, |&(t, _)| t) { Ok(_) => true, @@ -33,7 +33,7 @@ impl NumSet { } } - #[inline(always)] + #[inline] fn _contains_interval(&self, lower_bound: Time, upper_bound: Time) -> bool { assert!(lower_bound <= upper_bound); match self.0.binary_search_by_key(&lower_bound, |&(t, _)| t) { @@ -43,7 +43,7 @@ impl NumSet { } } - #[inline(always)] + #[inline] pub(super) fn contains_unbounded_interval(&self, lower_bound: Time) -> bool { self.0 .last() diff --git a/scan_promela/Cargo.toml b/scan_promela/Cargo.toml index 84a0abe..ff3d652 100644 --- a/scan_promela/Cargo.toml +++ b/scan_promela/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "smc_scan_promela" -version = "0.1.1" +version = "0.2.0" edition = "2024" description = "Promela frontend for the Scan model checker." documentation = "https://convince-project.github.io/scan/crates/scan_promela/index.html" @@ -9,11 +9,17 @@ repository = "https://github.com/convince-project/scan" license = "Apache-2.0" readme = "README.md" keywords = ["verification", "model-checking", "promela"] -categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] [lib] name = "scan_promela" # The name of the target. -crate-type = ["lib"] # The crate types to generate. +crate-type = ["lib"] # The crate types to generate. [build-dependencies] cfgrammar = "0.14" @@ -25,7 +31,8 @@ cfgrammar = "0.14" lrlex = "0.14.1" lrpar = "0.14.1" regex = "1" -smc_scan_core = { version = "0.1.1", path = "../scan_core" } +smc_scan_core = { version = "0.2.0", path = "../scan_core" } +smc_scan_pmtl = { version = "0.1.0", path = "../scan_pmtl" } anyhow = { workspace = true } log = { workspace = true } thiserror = { workspace = true } diff --git a/scan_promela/src/lib.rs b/scan_promela/src/lib.rs index 47d05a8..c2afa66 100644 --- a/scan_promela/src/lib.rs +++ b/scan_promela/src/lib.rs @@ -13,9 +13,10 @@ lrpar_mod!("spinv4.y"); pub mod builder; pub use builder::*; use regex::Regex; -use scan_core::{CsModel, PmtlOracle, Scan}; +use scan_core::{Scan, TransitionSystem}; +use scan_pmtl::PmtlOracle; -pub type PromelaScan = Scan; +pub type PromelaScan = Scan; pub type PromelaModel = (); @@ -89,7 +90,7 @@ fn process_file(path: &Path, debug_mode: bool) -> anyhow::Result<(PromelaScan, P let cs = Builder::create_channel_system(ast) .context("failed to create channel system from AST".to_string())?; info!("Channel system built successfully."); - let tsd = CsModel::new(cs); + let tsd = TransitionSystem::new(cs); let oracle = PmtlOracle::new(&[], &[]); let scan = Scan::new(tsd, oracle); Ok((scan, ())) diff --git a/scan_scxml/Cargo.toml b/scan_scxml/Cargo.toml index 5bb7778..66560d4 100644 --- a/scan_scxml/Cargo.toml +++ b/scan_scxml/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "smc_scan_scxml" -version = "0.2.0" +version = "0.3.0" edition = "2024" description = "SCXML frontend for the Scan model checker." documentation = "https://convince-project.github.io/scan/crates/scan_scxml/index.html" @@ -9,22 +9,28 @@ repository = "https://github.com/convince-project/scan" license = "Apache-2.0" readme = "README.md" keywords = ["verification", "model-checking", "scxml"] -categories = ["compilers", "concurrency", "parser-implementations", "science::robotics", "simulation"] +categories = [ + "compilers", + "concurrency", + "parser-implementations", + "science::robotics", + "simulation" +] [lib] name = "scan_scxml" # The name of the target. -crate-type = ["lib"] # The crate types to generate. +crate-type = ["lib"] # The crate types to generate. [dependencies] -smc_scan_core = { version = "0.1.1", path="../scan_core" } +smc_scan_core = { version = "0.2.0", path = "../scan_core" } +smc_scan_pmtl = { version = "0.1.0", path = "../scan_pmtl" } anyhow = { workspace = true } boa_ast = "0.21.1" boa_interner = "0.21.1" boa_parser = "0.21.1" log = { workspace = true } -quick-xml = "0.39.2" +quick-xml = "0.40.0" thiserror = { workspace = true } logos = "0.16.1" -chumsky = "0.12.0" +chumsky = "0.13.0" csv = { workspace = true } -flate2 = { workspace = true } diff --git a/scan_scxml/src/builder.rs b/scan_scxml/src/builder.rs index be4da66..0997888 100644 --- a/scan_scxml/src/builder.rs +++ b/scan_scxml/src/builder.rs @@ -4,12 +4,14 @@ mod expression; use self::expression::{expression, infer_type}; use crate::parser::{ - Executable, If, OmgBaseType, OmgType, OmgTypeDef, OmgTypes, Param, Parser, Scxml, Send, Target, + Executable, If, OmgBaseType, OmgType, OmgTypeDef, OmgTypes, Param, Parser, Scxml, Send, State, + Target, }; use anyhow::{Context, anyhow, bail}; use boa_interner::Interner; use log::{info, trace, warn}; use scan_core::{channel_system::*, *}; +use scan_pmtl::{Pmtl, PmtlOracle}; use std::collections::{BTreeMap, HashMap, HashSet}; // TODO: @@ -19,13 +21,15 @@ use std::collections::{BTreeMap, HashMap, HashSet}; #[derive(Debug, Clone)] pub struct ScxmlModel { // u16 here represents PgId + // TODO: turn into indexed Vec pub fsm_names: HashMap, // usize here represents event index pub parameters: HashMap, pub int_queues: HashSet, pub ext_queues: HashMap, pub events: Vec<(String, Option)>, - pub ports: Vec<(String, OmgType, Vec)>, + pub port_vars: Vec<(String, OmgType, Vec>)>, + pub ports: Vec, pub assumes: Vec, pub guarantees: Vec, pub omg_types: OmgTypes, @@ -66,8 +70,11 @@ pub struct ModelBuilder { // Properties guarantees: Vec<(String, Pmtl)>, assumes: Vec<(String, Pmtl)>, - predicates: Vec>, - ports: HashMap)>, + predicates: Vec>, + // port vars are (in general) expressions over atoms on the same channel + port_vars: HashMap>)>, + // ports are defined by a channel and a vec of init values. + ports: Vec<(Channel, Vec)>, // extra data int_queues: HashSet, } @@ -82,13 +89,35 @@ impl ModelBuilder { mut parser: Parser, properties: &[String], all_properties: bool, - ) -> anyhow::Result<(CsModel, PmtlOracle, ScxmlModel)> { + ) -> anyhow::Result<(TransitionSystem, PmtlOracle, ScxmlModel)> { let mut model_builder = ModelBuilder::default(); model_builder .prebuild_processes(&mut parser) .context("failed prebuilding processes")?; info!(target: "build", "Visit process list"); + // Make sure missing FSM are added as one-state FSMs. + for id in model_builder.fsm_builders.keys() { + if !parser.processes.contains_key(id) { + parser.processes.insert( + id.clone(), + Scxml { + name: id.clone(), + initial: String::from("init"), + datamodel: Vec::new(), + states: HashMap::from([( + String::from("init"), + State { + id: String::from("init"), + transitions: Vec::new(), + on_entry: Vec::new(), + on_exit: Vec::new(), + }, + )]), + }, + ); + } + } for (id, fsm) in parser.processes.iter() { model_builder .build_fsm(fsm, &mut parser.interner, &mut parser.types) @@ -123,7 +152,7 @@ impl ModelBuilder { fn add_fsm_builder(&mut self, id: &str) -> anyhow::Result<&FsmBuilder> { if self.fsm_builders.contains_key(id) { - bail!("FSM {id} aready exists"); + bail!("FSM {id} already exists"); } else { let pg_id = self.cs.new_program_graph(); let ext_queue = self @@ -856,7 +885,7 @@ impl ModelBuilder { } // Connect NULL events with named events - // by transitioning from last "NUll" location to dequeuing event location. + // by transitioning from last "NULL" location to dequeuing event location. self.cs .add_autonomous_transition(pg_id, null_trans, int_queue_loc, None)?; // Return to dequeue a new (internal or external) event. @@ -1188,7 +1217,7 @@ impl ModelBuilder { ); } } - // Retreive or create channel for parameter passing. + // Retrieve or create channel for parameter passing. let scan_types = exprs.iter().map(|expr| expr.r#type()).collect::>(); let param_chn = *self .parameter_channels @@ -1243,7 +1272,7 @@ impl ModelBuilder { ) })? .clone(); - let init = expression::( + let init = expression::>( init, &parser.interner, &HashMap::new(), @@ -1261,7 +1290,7 @@ impl ModelBuilder { .parameter_channels .get(&(origin, target, event_id)) .expect("parameters' channel for event in port"); - self.ports.insert( + self.port_vars.insert( port_id.to_owned(), ( param_type.ok_or_else(|| { @@ -1269,34 +1298,86 @@ impl ModelBuilder { })?, init.iter() .enumerate() - .map(|(param_idx, &init)| { - (Atom::State(*channel, param_start_idx + param_idx), init) + .map(|(param_idx, init)| { + Expression::from_var( + Atom::State(*channel, param_start_idx + param_idx), + init.r#type(), + ) }) .collect(), ), ); + + let index = match self.ports.binary_search_by_key(channel, |(ch, _)| *ch) { + Ok(index) => index, + Err(index) => { + let default = event_builder + .params + .values() + .flat_map(|omg_type| { + omg_type + .as_ref() + .ok_or_else(|| { + anyhow!( + "type of param {param} for port {port_id} not found" + ) + }) + .expect("omg type") + .to_scan_types(&parser.types) + .expect("omg type to scan type") + .into_iter() + .map(|t| t.default_value()) + }) + .collect::>(); + self.ports.insert(index, (*channel, default)); + index + } + }; + init.iter().enumerate().for_each(|(param_idx, init)| { + self.ports[index].1[param_start_idx + param_idx] = *init + }); } else { - let channel = target_builder.ext_queue; - self.ports.insert( - port_id.to_owned(), - ( - OmgType::Base(OmgBaseType::Boolean), - vec![( - Atom::Event(Event { - pg_id: origin, - channel, - event_type: EventType::Send( - vec![ - Val::Natural(event_id as Natural), - Val::Natural(u16::from(origin) as Natural), - ] - .into(), + // If the event has params, + // we consider the receiving of a message in the dedicated param channel; + // otherwise, we consider every event on the external queue and test for the event/origin to match. + if let Some(&channel) = self.parameter_channels.get(&(origin, target, event_id)) { + self.port_vars.insert( + port_id.to_owned(), + ( + OmgType::Base(OmgBaseType::Boolean), + vec![Expression::Boolean(BooleanExpr::Var(Atom::Event(channel)))], + ), + ); + } else { + let ext_queue = target_builder.ext_queue; + self.port_vars.insert( + port_id.to_owned(), + ( + OmgType::Base(OmgBaseType::Boolean), + vec![Expression::Boolean(BooleanExpr::And(vec![ + BooleanExpr::Var(Atom::Event(ext_queue)), + BooleanExpr::NatEqual( + NaturalExpr::Var(Atom::State(ext_queue, 0)), + NaturalExpr::Const(event_id as Natural), ), - }), - Val::Boolean(false), - )], - ), - ); + BooleanExpr::NatEqual( + NaturalExpr::Var(Atom::State(ext_queue, 1)), + NaturalExpr::Const(u16::from(origin) as Natural), + ), + ]))], + ), + ); + // Default values represent a non-existing event/origin + if let Err(index) = self.ports.binary_search_by_key(&ext_queue, |(ch, _)| *ch) { + self.ports.insert( + index, + ( + ext_queue, + vec![Val::from(Natural::MAX), Val::from(Natural::MAX)], + ), + ); + } + } } } Ok(()) @@ -1312,75 +1393,48 @@ impl ModelBuilder { let predicate = expression( predicate, &parser.interner, - &self - .ports - .iter() - .map(|(name, (omg_type, atoms))| { - ( - name.clone(), - ( - omg_type.clone(), - atoms - .iter() - .map(|(atom, val)| (atom.clone(), val.r#type())) - .collect(), - ), - ) - }) - .collect(), + &self.port_vars, Some(&OmgType::Base(OmgBaseType::Boolean)), &mut parser.types, ) .with_context(|| format!("failed building predicate {predicate:?}"))?; if predicate.len() != 1 { - bail!("predicate must be a boolean expression"); + bail!("predicate is not a boolean expression"); + } else if let Expression::Boolean(predicate) = + predicate.first().expect("len of predicate is 1") + { + self.predicates.push(predicate.clone()); + } else { + bail!("predicate is not a boolean expression"); } - let predicate = predicate[0].clone(); - self.predicates.push(predicate); } - self.guarantees = parser - .properties - .guarantees - .iter() - .filter(|(name, _)| all_properties || properties.contains(name)) - .cloned() - .collect(); + if !all_properties { + parser + .properties + .guarantees + .retain(|(name, _)| properties.contains(name)); + } + self.guarantees = parser.properties.guarantees.clone(); self.assumes = parser.properties.assumes.clone(); Ok(()) } - fn build_model(self, parser: Parser) -> (CsModel, PmtlOracle, ScxmlModel) { - let mut model = CsModel::new(self.cs); - let mut ports = Vec::new(); - for (port_name, (_omg_type, atoms)) in self.ports { - // TODO FIXME handle error. - // NOTE: all atoms in the same port must have the same channel - if let Some((Atom::State(channel, _), _)) = atoms.first().cloned() { - let (param_idxs, types): (Vec, _) = atoms - .into_iter() - .map(|(atom, init)| { - if let Atom::State(c, param_idx) = atom { - assert_eq!(channel, c); - model.add_port(channel, param_idx, init); - (param_idx, init.r#type()) - } else { - panic!("all atoms are of state type") - } - }) - .unzip(); - ports.push((channel, param_idxs, port_name, _omg_type, types)); - } - } - // Ports need to be sorted by channel or will not match state iterator - ports.sort_by_key(|(c, idxs, ..)| (*c, *idxs.first().expect("at least a value"))); - let ports = ports + fn build_model(mut self, parser: Parser) -> (TransitionSystem, PmtlOracle, ScxmlModel) { + let mut model = TransitionSystem::new(self.cs); + let port_vars = self + .port_vars .into_iter() - .map(|(_, _, name, omg_type, types)| (name, omg_type, types)) - .collect(); + .map(|(name, (omg_type, exprs))| (name, omg_type, exprs)) + .collect::>(); + self.ports.sort_unstable_by_key(|(c, _)| *c); + for (channel, init) in &self.ports { + model.add_port(*channel, init.clone()); + } for pred_expr in self.predicates { - // TODO FIXME handle error. - let _id = model.add_predicate(pred_expr); + model.add_predicate(pred_expr); } + // Shrink model storage (just an optimization); + model.shrink(); let (guarantee_names, guarantees): (Vec<_>, Vec<_>) = self.guarantees.into_iter().unzip(); let (assume_names, assumes): (Vec<_>, Vec<_>) = self.assumes.into_iter().unzip(); let oracle = PmtlOracle::new(assumes.as_slice(), guarantees.as_slice()); @@ -1419,10 +1473,11 @@ impl ModelBuilder { .collect(), int_queues: self.int_queues, events, - ports, + port_vars, assumes: assume_names, guarantees: guarantee_names, omg_types: parser.types, + ports: self.ports.iter().map(|(c, _)| *c).collect(), }, ) } diff --git a/scan_scxml/src/builder/expression.rs b/scan_scxml/src/builder/expression.rs index ee38255..d9ba4e2 100644 --- a/scan_scxml/src/builder/expression.rs +++ b/scan_scxml/src/builder/expression.rs @@ -236,25 +236,27 @@ pub(super) fn infer_type( } } -// WARN: vars and params have the same type so they could be easily swapped by mistake when calling the function. -pub(super) fn expression( +pub(super) fn expression( expr: &boa_ast::Expression, interner: &Interner, - vars: &HashMap)>, + vars: &HashMap)>, expr_type: Option<&OmgType>, omg_types: &mut OmgTypes, -) -> anyhow::Result>> { +) -> anyhow::Result>> +where + V: Copy, + E: Clone + Into>, +{ let expr = match expr { boa_ast::Expression::This(_this) => todo!(), boa_ast::Expression::Identifier(ident) => { let ident = ident.to_interned_string(interner); vars.get(&ident) - .map(|(_, vars)| { - vars.iter() - .map(|(var, r#type)| Expression::from_var(var.clone(), *r#type)) - .collect::>>() - }) .ok_or(anyhow!("unknown identifier: {ident}"))? + .1 + .iter() + .map(|t| t.clone().into()) + .collect() } boa_ast::Expression::Literal(lit) => { use boa_ast::expression::literal::LiteralKind; diff --git a/scan_scxml/src/lib.rs b/scan_scxml/src/lib.rs index c98b572..49fd272 100644 --- a/scan_scxml/src/lib.rs +++ b/scan_scxml/src/lib.rs @@ -10,9 +10,10 @@ pub use builder::ScxmlModel; use log::info; pub use print_trace::TracePrinter; pub use scan_core; -use scan_core::{CsModel, PmtlOracle, Scan}; +use scan_core::Scan; +use scan_pmtl::PmtlOracle; -pub type ScxmlScan = Scan; +pub type ScxmlScan = Scan; pub fn load( path: &Path, diff --git a/scan_scxml/src/parser.rs b/scan_scxml/src/parser.rs index b3d4d49..a88a122 100644 --- a/scan_scxml/src/parser.rs +++ b/scan_scxml/src/parser.rs @@ -18,6 +18,7 @@ use boa_interner::Interner; use log::warn; use log::{error, info, trace}; use quick_xml::Reader; +use quick_xml::XmlVersion; use quick_xml::events::Event; use std::collections::HashMap; use std::io::BufRead; @@ -73,13 +74,14 @@ fn attrs( tag: quick_xml::events::BytesStart<'_>, keys: &[&str], opt_keys: &[&str], + xml_version: XmlVersion, ) -> anyhow::Result> { let mut attrs = HashMap::new(); for attr in tag.attributes() { let attr = attr?; let key = str::from_utf8(attr.key.into_inner())?; if keys.contains(&key) || opt_keys.contains(&key) { - let val = attr.unescape_value()?.to_string(); + let val = attr.normalized_value(xml_version)?.to_string(); attrs.insert(key.to_string(), val); } else { error!(target: "parser", "found unknown attribute '{key}'"); @@ -247,6 +249,7 @@ impl Parser { ) -> anyhow::Result<()> { let mut buf = Vec::new(); let mut stack = Vec::new(); + let mut xml_version = XmlVersion::Implicit1_0; loop { match reader .read_event_into(&mut buf) @@ -297,7 +300,7 @@ impl Parser { .last() .is_some_and(|e| *e == ConvinceTag::Specification) => { - let attrs = attrs(tag, &[ATTR_PATH], &[]) + let attrs = attrs(tag, &[ATTR_PATH], &[], xml_version) .context("failed to parse 'types' tag attributes")?; let mut path = parent.to_owned(); path.extend(&PathBuf::from(attrs.get(ATTR_PATH).unwrap())); @@ -316,7 +319,7 @@ impl Parser { .last() .is_some_and(|e| *e == ConvinceTag::Specification) => { - let attrs = attrs(tag, &[ATTR_PATH], &[]) + let attrs = attrs(tag, &[ATTR_PATH], &[], xml_version) .context("failed to parse 'properties' tag attributes")?; let mut path = parent.to_owned(); path.extend(&PathBuf::from(attrs.get(ATTR_PATH).unwrap())); @@ -337,7 +340,7 @@ impl Parser { TAG_PROCESS if stack.last().is_some_and(|e| *e == ConvinceTag::ProcessList) => { - let attrs = attrs(tag, &[ATTR_ID, ATTR_PATH], &[ATTR_MOC]) + let attrs = attrs(tag, &[ATTR_ID, ATTR_PATH], &[ATTR_MOC], xml_version) .context("failed to parse 'process' tag attributes")?; if let Some(moc) = attrs.get(ATTR_MOC) && moc != "fsm" @@ -386,7 +389,9 @@ impl Parser { Event::CData(_) => { return Err(anyhow!("CData not supported")); } - Event::Decl(_) => continue, + Event::Decl(decl) => { + xml_version = decl.xml_version()?; + } Event::PI(_) => { return Err(anyhow!("Processing Instructions not supported")); } diff --git a/scan_scxml/src/parser/fsm.rs b/scan_scxml/src/parser/fsm.rs index 77d1817..44ab68c 100644 --- a/scan_scxml/src/parser/fsm.rs +++ b/scan_scxml/src/parser/fsm.rs @@ -6,7 +6,7 @@ use boa_ast::scope::Scope; use boa_interner::Interner; use log::{error, info, trace}; use quick_xml::events::Event; -use quick_xml::{Reader, events}; +use quick_xml::{Reader, XmlVersion, events}; use scan_core::Time; use std::collections::HashMap; use std::fmt::Debug; @@ -62,8 +62,9 @@ impl Data { omg_type: Option, interner: &mut Interner, omg_types: &OmgTypes, + xml_version: XmlVersion, ) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_ID], &[ATTR_EXPR, ATTR_TYPE])?; + let attrs = attrs(tag, &[ATTR_ID], &[ATTR_EXPR, ATTR_TYPE], xml_version)?; let id = attrs[ATTR_ID].to_string(); let omg_type = attrs .get(ATTR_TYPE) @@ -100,8 +101,8 @@ pub struct State { } impl State { - fn parse(tag: events::BytesStart<'_>) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_ID], &[])?; + fn parse(tag: events::BytesStart<'_>, xml_version: XmlVersion) -> anyhow::Result { + let attrs = attrs(tag, &[ATTR_ID], &[], xml_version)?; Ok(State { id: attrs[ATTR_ID].clone(), transitions: Vec::new(), @@ -129,8 +130,12 @@ pub struct Transition { } impl Transition { - fn parse(tag: events::BytesStart<'_>, interner: &mut Interner) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_TARGET], &[ATTR_EVENT, ATTR_COND])?; + fn parse( + tag: events::BytesStart<'_>, + interner: &mut Interner, + xml_version: XmlVersion, + ) -> anyhow::Result { + let attrs = attrs(tag, &[ATTR_TARGET], &[ATTR_EVENT, ATTR_COND], xml_version)?; let cond = attrs .get(ATTR_COND) .map(|expression| ecmascript(expression, &Scope::new_global(), interner)) @@ -173,8 +178,11 @@ pub enum Executable { } impl Executable { - fn parse_raise(tag: events::BytesStart<'_>) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_EVENT], &[])?; + fn parse_raise( + tag: events::BytesStart<'_>, + xml_version: XmlVersion, + ) -> anyhow::Result { + let attrs = attrs(tag, &[ATTR_EVENT], &[], xml_version)?; let event = attrs[ATTR_EVENT].clone(); Ok(Executable::Raise { event }) } @@ -182,8 +190,9 @@ impl Executable { fn parse_assign( tag: events::BytesStart<'_>, interner: &mut Interner, + xml_version: XmlVersion, ) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_LOCATION, ATTR_EXPR], &[])?; + let attrs = attrs(tag, &[ATTR_LOCATION, ATTR_EXPR], &[], xml_version)?; let location = attrs[ATTR_LOCATION].clone(); let expr = ecmascript(attrs[ATTR_EXPR].as_str(), &Scope::new_global(), interner)?; Ok(Executable::Assign { location, expr }) @@ -223,11 +232,16 @@ pub struct Send { } impl Send { - fn parse(tag: events::BytesStart<'_>, interner: &mut Interner) -> anyhow::Result { + fn parse( + tag: events::BytesStart<'_>, + interner: &mut Interner, + xml_version: XmlVersion, + ) -> anyhow::Result { let attrs = attrs( tag, &[ATTR_EVENT], &[ATTR_TARGET, ATTR_TARGETEXPR, ATTR_DELAY], + xml_version, )?; let target = if let Some(target) = attrs.get(ATTR_TARGET) { Some(Target::Id(target.to_string())) @@ -264,8 +278,9 @@ impl If { fn parse( tag: events::BytesStart<'_>, interner: &mut Interner, + xml_version: XmlVersion, ) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_COND], &[])?; + let attrs = attrs(tag, &[ATTR_COND], &[], xml_version)?; ecmascript(attrs[ATTR_COND].as_str(), &Scope::new_global(), interner) } } @@ -283,8 +298,14 @@ impl Param { omg_type: Option, interner: &mut Interner, omg_types: &OmgTypes, + xml_version: XmlVersion, ) -> anyhow::Result { - let attrs = attrs(tag, &[ATTR_NAME], &[ATTR_TYPE, ATTR_LOCATION, ATTR_EXPR])?; + let attrs = attrs( + tag, + &[ATTR_NAME], + &[ATTR_TYPE, ATTR_LOCATION, ATTR_EXPR], + xml_version, + )?; let name = attrs[ATTR_NAME].clone(); let omg_type = omg_type.or_else(|| { attrs @@ -315,11 +336,12 @@ pub struct Scxml { } impl Scxml { - fn parse(tag: events::BytesStart<'_>) -> anyhow::Result { + fn parse(tag: events::BytesStart<'_>, xml_version: XmlVersion) -> anyhow::Result { let attrs = attrs( tag, &[ATTR_NAME, ATTR_INITIAL], &[ATTR_VERSION, ATTR_DATAMODEL, ATTR_XMLNS, ATTR_MODEL_SRC], + xml_version, ) .with_context(|| format!("failed to parse '{TAG_SCXML}' tag attributes"))?; Ok(Scxml { @@ -339,6 +361,7 @@ pub(super) fn parse( let mut buf = Vec::new(); let mut stack: Vec = Vec::new(); let mut type_annotation: Option = None; + let mut xml_version = XmlVersion::Implicit1_0; info!(target: "parser", "parsing fsm"); loop { match reader @@ -351,7 +374,7 @@ pub(super) fn parse( .decode(tag.name().into_inner())? .into_owned(); trace!(target: "parser", "start tag '{tag_name}'"); - let tag_obj = parse_start_tag(tag_name, &stack, tag, interner)?; + let tag_obj = parse_start_tag(tag_name, &stack, tag, interner, xml_version)?; stack.push(tag_obj); type_annotation = None; } @@ -447,6 +470,7 @@ pub(super) fn parse( &mut type_annotation.take(), interner, omg_types, + xml_version, )?; } Event::Text(text) => { @@ -468,7 +492,7 @@ pub(super) fn parse( Event::CData(_) => { bail!("CData not supported"); } - Event::Decl(_) => continue, + Event::Decl(decl) => xml_version = decl.xml_version()?, Event::PI(_) => { bail!("Processing Instructions not supported"); } @@ -495,6 +519,7 @@ fn parse_empty_tag( type_annotation: &mut Option, interner: &mut Interner, omg_types: &OmgTypes, + xml_version: XmlVersion, ) -> Result<(), anyhow::Error> { trace!(target: "parser", "'{tag_name}' empty tag"); match tag_name.as_str() { @@ -503,8 +528,14 @@ fn parse_empty_tag( .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::Datamodel(_))) => { - let data = Data::parse(tag, type_annotation.take(), interner, omg_types) - .with_context(|| ParserError::Tag(tag_name))?; + let data = Data::parse( + tag, + type_annotation.take(), + interner, + omg_types, + xml_version, + ) + .with_context(|| ParserError::Tag(tag_name))?; Data::push(data, stack)?; } TAG_STATE @@ -512,7 +543,8 @@ fn parse_empty_tag( .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::Scxml(_))) => { - let state = State::parse(tag).with_context(|| ParserError::Tag(tag_name))?; + let state = + State::parse(tag, xml_version).with_context(|| ParserError::Tag(tag_name))?; state.push(stack)?; } TAG_TRANSITION @@ -520,21 +552,23 @@ fn parse_empty_tag( .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::State(_))) => { - let transition = - Transition::parse(tag, interner).with_context(|| ParserError::Tag(tag_name))?; + let transition = Transition::parse(tag, interner, xml_version) + .with_context(|| ParserError::Tag(tag_name))?; transition.push(stack)?; } // we `rev()` the iterator only because we expect the relevant tag to be towards the end of the stack TAG_RAISE if stack.last().is_some_and(|tag| tag.is_executable()) => { - let raise = Executable::parse_raise(tag).with_context(|| ParserError::Tag(tag_name))?; + let raise = Executable::parse_raise(tag, xml_version) + .with_context(|| ParserError::Tag(tag_name))?; raise.push(stack)?; } TAG_SEND if stack.last().is_some_and(|tag| tag.is_executable()) => { - let send = Send::parse(tag, interner).with_context(|| ParserError::Tag(tag_name))?; + let send = Send::parse(tag, interner, xml_version) + .with_context(|| ParserError::Tag(tag_name))?; Executable::Send(send).push(stack)?; } TAG_ASSIGN if stack.last().is_some_and(|tag| tag.is_executable()) => { - let assign = Executable::parse_assign(tag, interner) + let assign = Executable::parse_assign(tag, interner, xml_version) .with_context(|| ParserError::Tag(tag_name))?; assign.push(stack)?; } @@ -543,8 +577,14 @@ fn parse_empty_tag( .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::Send(_))) => { - let param = Param::parse(tag, type_annotation.take(), interner, omg_types) - .with_context(|| ParserError::Tag(tag_name))?; + let param = Param::parse( + tag, + type_annotation.take(), + interner, + omg_types, + xml_version, + ) + .with_context(|| ParserError::Tag(tag_name))?; if let ScxmlTag::Send(send) = stack.last_mut().expect("param must be inside other tag") { send.params.push(param); @@ -573,7 +613,8 @@ fn parse_empty_tag( .is_some_and(|tag| matches!(tag, ScxmlTag::If(_))) => { if let Some(ScxmlTag::If(r#if)) = stack.last_mut() { - let cond = If::parse(tag, interner).with_context(|| ParserError::Tag(tag_name))?; + let cond = If::parse(tag, interner, xml_version) + .with_context(|| ParserError::Tag(tag_name))?; r#if.elif.push((cond, Vec::new())); } else { unreachable!() @@ -592,9 +633,10 @@ fn parse_start_tag( stack: &[ScxmlTag], tag: events::BytesStart<'_>, interner: &mut Interner, + xml_version: XmlVersion, ) -> Result { match tag_name.as_str() { - TAG_SCXML if stack.is_empty() => Scxml::parse(tag).map(ScxmlTag::Scxml), + TAG_SCXML if stack.is_empty() => Scxml::parse(tag, xml_version).map(ScxmlTag::Scxml), TAG_DATAMODEL if stack .last() @@ -607,24 +649,26 @@ fn parse_start_tag( .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::Scxml(_))) => { - State::parse(tag).map(ScxmlTag::State) + State::parse(tag, xml_version).map(ScxmlTag::State) } TAG_TRANSITION if stack .last() .is_some_and(|tag| matches!(*tag, ScxmlTag::State(_))) => { - Transition::parse(tag, interner).map(ScxmlTag::Transition) + Transition::parse(tag, interner, xml_version).map(ScxmlTag::Transition) } TAG_SEND if stack.iter().rev().any(|tag| tag.is_executable()) => { - Send::parse(tag, interner).map(ScxmlTag::Send) + Send::parse(tag, interner, xml_version).map(ScxmlTag::Send) + } + TAG_IF if stack.iter().rev().any(|tag| tag.is_executable()) => { + If::parse(tag, interner, xml_version) + .map(|cond| If { + elif: vec![(cond, Vec::new())], + r#else: None, + }) + .map(ScxmlTag::If) } - TAG_IF if stack.iter().rev().any(|tag| tag.is_executable()) => If::parse(tag, interner) - .map(|cond| If { - elif: vec![(cond, Vec::new())], - r#else: None, - }) - .map(ScxmlTag::If), TAG_ONENTRY if stack .last() diff --git a/scan_scxml/src/parser/property.rs b/scan_scxml/src/parser/property.rs index f6b6e3b..412391f 100644 --- a/scan_scxml/src/parser/property.rs +++ b/scan_scxml/src/parser/property.rs @@ -4,8 +4,8 @@ use anyhow::{Context, anyhow, bail}; use boa_ast::scope::Scope; use boa_interner::Interner; use log::{error, info, trace}; -use quick_xml::{Reader, events::Event}; -use scan_core::Pmtl; +use quick_xml::{Reader, XmlVersion, events::Event}; +use scan_pmtl::Pmtl; use std::{ collections::HashMap, io::{BufRead, Read}, @@ -78,6 +78,7 @@ impl Properties { ) -> anyhow::Result<()> { let mut buf = Vec::new(); let mut stack: Vec = Vec::new(); + let mut xml_version = XmlVersion::Implicit1_0; info!("parsing properties"); loop { match reader @@ -104,10 +105,15 @@ impl Properties { .last() .is_some_and(|tag| matches!(*tag, PropertyTag::Ports)) => { - let attrs = attrs(tag, &[ATTR_EVENT, ATTR_ORIGIN, ATTR_TARGET], &[]) - .with_context(|| { - format!("failed to parse '{TAG_PORT}' tag attributes") - })?; + let attrs = attrs( + tag, + &[ATTR_EVENT, ATTR_ORIGIN, ATTR_TARGET], + &[], + xml_version, + ) + .with_context(|| { + format!("failed to parse '{TAG_PORT}' tag attributes") + })?; stack.push(PropertyTag::Port( attrs[ATTR_EVENT].clone(), attrs[ATTR_ORIGIN].clone(), @@ -157,9 +163,9 @@ impl Properties { .is_some_and(|tag| matches!(*tag, PropertyTag::Port(_, _, _))) => { if let Some(PropertyTag::Port(event, origin, target)) = stack.last() { - let attrs = attrs(tag, &[ATTR_ID], &[]).with_context(|| { - format!("failed to parse '{TAG_EVENT_VAR}' tag attributes") - })?; + let attrs = attrs(tag, &[ATTR_ID], &[], xml_version).with_context( + || format!("failed to parse '{TAG_EVENT_VAR}' tag attributes"), + )?; let id = attrs[ATTR_ID].clone(); self.ports.insert( id, @@ -182,11 +188,15 @@ impl Properties { { if let Some(PropertyTag::Port(event, origin, target)) = stack.last_mut() { - let attrs = - attrs(tag, &[ATTR_ID, ATTR_PARAM, ATTR_EXPR, ATTR_TYPE], &[]) - .with_context(|| { - format!("failed to parse '{TAG_STATE_VAR}' tag attributes") - })?; + let attrs = attrs( + tag, + &[ATTR_ID, ATTR_PARAM, ATTR_EXPR, ATTR_TYPE], + &[], + xml_version, + ) + .with_context(|| { + format!("failed to parse '{TAG_STATE_VAR}' tag attributes") + })?; let expression = ecmascript( attrs[ATTR_EXPR].as_str(), &Scope::new_global(), @@ -211,10 +221,11 @@ impl Properties { } } TAG_PROPERTY => { - let attrs = attrs(tag, &[ATTR_ID, ATTR_EXPR], &[ATTR_LOGIC]) - .with_context(|| { - format!("failed to parse '{TAG_PROPERTY}' tag attributes") - })?; + let attrs = + attrs(tag, &[ATTR_ID, ATTR_EXPR], &[ATTR_LOGIC], xml_version) + .with_context(|| { + format!("failed to parse '{TAG_PROPERTY}' tag attributes") + })?; let id = attrs[ATTR_ID].to_owned(); let expr = attrs[ATTR_EXPR].as_str(); let formula = super::rye::parse(expr) @@ -258,7 +269,9 @@ impl Properties { Event::CData(_) => { return Err(anyhow!("CData not supported")); } - Event::Decl(_) => continue, + Event::Decl(decl) => { + xml_version = decl.xml_version()?; + } Event::PI(_) => { return Err(anyhow!("Processing Instructions not supported")); } diff --git a/scan_scxml/src/parser/rye.rs b/scan_scxml/src/parser/rye.rs index d6d931a..ba67915 100644 --- a/scan_scxml/src/parser/rye.rs +++ b/scan_scxml/src/parser/rye.rs @@ -1,7 +1,8 @@ use anyhow::{anyhow, bail}; use chumsky::{IterParser, Parser, prelude::*, select}; use logos::Logos; -use scan_core::{Pmtl, Time}; +use scan_core::Time; +use scan_pmtl::Pmtl; #[derive(Logos, Debug, PartialEq, Eq, Hash, Clone)] #[logos(skip r"[ \t\n]+")] diff --git a/scan_scxml/src/print_trace.rs b/scan_scxml/src/print_trace.rs index 89ef01f..9979d18 100644 --- a/scan_scxml/src/print_trace.rs +++ b/scan_scxml/src/print_trace.rs @@ -1,123 +1,86 @@ use crate::parser::{OmgBaseType, OmgType, OmgTypeDef, OmgTypes}; use super::ScxmlModel; -use scan_core::channel_system::{Event, EventType}; -use scan_core::{RunOutcome, Time, Tracer, Val}; -use std::{ - env::current_dir, - fs::{File, create_dir, create_dir_all, exists, remove_file, rename}, - path::PathBuf, - sync::{Arc, atomic::AtomicU32}, -}; +use scan_core::channel_system::{Action, Event, EventType}; +use scan_core::{Time, TraceWriter, Tracer, Val}; #[derive(Debug)] -pub struct TracePrinter<'a> { - index: Arc, - path: PathBuf, - writer: Option>>, - model: &'a ScxmlModel, +pub struct TracePrinter { + writer: csv::Writer, } -impl<'a> TracePrinter<'a> { - const FOLDER: &'static str = "traces"; - const TEMP: &'static str = ".temp"; - const SUCCESSES: &'static str = "successes"; - const FAILURES: &'static str = "failures"; - const HEADER: [&'static str; 5] = ["Time", "Origin", "Target", "Event", "Values"]; - - pub fn new(model: &'a ScxmlModel) -> Self { - let mut path = current_dir().expect("current dir"); - for i in 0.. { - path.push(format!("{}_{i:02}", Self::FOLDER)); - if std::fs::create_dir(&path).is_ok() { - path.push(Self::TEMP); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - path.push(Self::SUCCESSES); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - path.push(Self::FAILURES); - create_dir(&path).expect("create temp dir"); - assert!(path.pop()); - break; - } else { - assert!(path.pop()); - } - } - - Self { - index: Arc::new(AtomicU32::new(0)), - path, - writer: None, - model, - } +impl Drop for TracePrinter { + fn drop(&mut self) { + self.writer.flush().expect("flush writer"); } +} - fn format_state>(&self, ports: I) -> Vec { - let mut iter = ports.into_iter(); - self.model - .ports +impl TracePrinter { + const HEADER: [&'static str; 5] = ["Time", "Event", "Origin", "Target", "Values"]; + + fn format_state(&self, model: &ScxmlModel, event: &Event, ports: &[Vec]) -> Vec { + // Assumes model.port_vals are ordered + model + .port_vars .iter() - .map(move |(_, omg_type, types)| { + .map(move |(_, omg_type, exprs)| { format_val( - iter.by_ref() - .take(types.len()) + exprs + .iter() + .map(|expr| { + expr.eval_deterministic(&|atom| match atom { + scan_core::Atom::State(channel, i) => ports + .get(model.ports.binary_search(&channel).unwrap()) + .unwrap()[i], + scan_core::Atom::Event(channel) => { + if event.channel == channel + && let EventType::Send(_) = event.event_type + { + Val::from(true) + } else { + Val::from(false) + } + } + }) + }) .collect::>() .as_slice(), omg_type, - &self.model.omg_types, + &model.omg_types, ) }) .collect() } } -impl<'a> Clone for TracePrinter<'a> { - fn clone(&self) -> Self { - // Get the temp folder - let mut path = self.path.clone(); - if path.is_file() { - path.pop(); - } - Self { - index: Arc::clone(&self.index), - path, - writer: None, - model: self.model, - } - } -} +impl Tracer for TracePrinter { + const EXTENSION: &'static str = "csv"; + + type ModelData = ScxmlModel; -impl<'a> Tracer for TracePrinter<'a> { - fn init(&mut self) { - let idx = self - .index - .fetch_add(1, std::sync::atomic::Ordering::Relaxed); - let filename = PathBuf::new() - .with_file_name(format!("{idx:04}")) - .with_extension("csv"); - self.path.push(Self::TEMP); - self.path.push(&filename); - self.path.add_extension("gz"); - let file = File::create_new(&self.path).expect("create file"); - let enc = flate2::GzBuilder::new() - .filename(filename.to_str().expect("file name")) - .comment("Scan-generated execution trace") - .write(file, flate2::Compression::best()); - let mut writer = csv::WriterBuilder::new().from_writer(enc); + fn init(writer: TraceWriter, data: &ScxmlModel) -> Self { + let mut writer = csv::Writer::from_writer(writer); writer .write_record( Self::HEADER.into_iter().map(String::from).chain( - self.model.ports.iter().map(|(name, omg_type, _)| { + data.port_vars.iter().map(|(name, omg_type, _)| { format!("{name}: {}", format_omg_type(omg_type)) }), ), ) .expect("write header"); - self.writer = Some(writer); + + Self { writer } } - fn trace>(&mut self, event: &Event, time: Time, ports: I) { + fn trace( + &mut self, + data: &ScxmlModel, + _action: Action, + event: &Event, + time: Time, + ports: &[Vec], + ) { let mut fields = Vec::new(); let time = time.to_string(); let origin_name; @@ -127,31 +90,22 @@ impl<'a> Tracer for TracePrinter<'a> { let mut params = String::new(); fields.push(time.as_str()); - if let Some((src, trg, event_idx)) = self.model.parameters.get(&event.channel) { - origin_name = self.model.fsm_names.get(&(*src).into()).unwrap().to_owned(); - target_name = self.model.fsm_names.get(&(*trg).into()).unwrap().to_owned(); - (event_name, param_types) = self.model.events.get(*event_idx).unwrap().clone(); + if let Some((src, trg, event_idx)) = data.parameters.get(&event.channel) { + origin_name = data.fsm_names.get(&(*src).into()).unwrap().to_owned(); + target_name = data.fsm_names.get(&(*trg).into()).unwrap().to_owned(); + (event_name, param_types) = data.events.get(*event_idx).unwrap().clone(); if let EventType::Send(ref vals) = event.event_type { - params = format_val_from_def( - vals, - param_types.as_ref().unwrap(), - &self.model.omg_types, - true, - ); + params = + format_val_from_def(vals, param_types.as_ref().unwrap(), &data.omg_types, true); } else { return; } - } else if let Some(trg) = self.model.ext_queues.get(&event.channel) { - target_name = self.model.fsm_names.get(&(*trg).into()).unwrap().to_owned(); + } else if let Some(trg) = data.ext_queues.get(&event.channel) { + target_name = data.fsm_names.get(&(*trg).into()).unwrap().to_owned(); if let EventType::Send(ref vals) = event.event_type { if let (Val::Natural(sent_event), Val::Natural(origin)) = (vals[0], vals[1]) { - origin_name = self - .model - .fsm_names - .get(&(origin as u16)) - .unwrap() - .to_owned(); - (event_name, param_types) = self.model.events[sent_event as usize].clone(); + origin_name = data.fsm_names.get(&(origin as u16)).unwrap().to_owned(); + (event_name, param_types) = data.events[sent_event as usize].clone(); if param_types.is_some() { // No need to trace this as parameters event already traced return; @@ -162,17 +116,12 @@ impl<'a> Tracer for TracePrinter<'a> { } else { return; } - } else if self.model.int_queues.contains(&event.channel) { - origin_name = self - .model - .fsm_names - .get(&event.pg_id.into()) - .unwrap() - .to_owned(); + } else if data.int_queues.contains(&event.channel) { + origin_name = data.fsm_names.get(&event.pg_id.into()).unwrap().to_owned(); target_name = origin_name.clone(); if let EventType::Send(ref vals) = event.event_type { if let Val::Natural(sent_event) = vals[0] { - (event_name, param_types) = self.model.events[sent_event as usize].clone(); + (event_name, param_types) = data.events[sent_event as usize].clone(); if param_types.is_some() { // No need to trace this as parameters event already traced return; @@ -187,53 +136,15 @@ impl<'a> Tracer for TracePrinter<'a> { panic!("Events should all be either internal or external events"); } - let state = self.format_state(ports); + let state = self.format_state(data, event, ports); self.writer - .as_mut() - .unwrap() .write_record( - [time, origin_name, target_name, event_name, params] + [time, event_name, origin_name, target_name, params] .into_iter() .chain(state), ) .expect("write record"); } - - fn finalize(self, outcome: &RunOutcome) { - let mut writer = self.writer.unwrap(); - writer.flush().expect("flush csv content"); - writer - .into_inner() - .expect("encoder") - .try_finish() - .expect("finish"); - - let mut new_path = self.path.clone(); - // pop file name - new_path.pop(); - // pop temp folder - new_path.pop(); - match outcome { - RunOutcome::Verified(verified) => { - if verified.iter().all(|b| *b) { - new_path.push(Self::SUCCESSES); - } else { - new_path.push(Self::FAILURES); - // This path might not exist yet - if !exists(new_path.as_path()).expect("check folder") { - create_dir_all(new_path.clone()).expect("create missing folder"); - } - } - } - RunOutcome::Incomplete => { - remove_file(&self.path).expect("delete file"); - return; - } - } - - new_path.push(self.path.file_name().expect("file name")); - rename(&self.path, new_path).expect("renaming"); - } } fn format_omg_type(omg_type: &OmgType) -> String { diff --git a/src/lib.rs b/src/lib.rs index 991f94f..942db32 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -21,13 +21,13 @@ mod report; mod trace; mod verify; -use std::{path::PathBuf, sync::Arc}; +use std::{env::current_dir, path::PathBuf}; use anyhow::{anyhow, bail}; use clap::{Parser, Subcommand, ValueEnum}; use progress::Bar; use report::Report; -use scan_core::{CsModel, MtlOracle, Oracle, PgModel, PmtlOracle, Scan, TransitionSystemGenerator}; +use scan_core::{Oracle, Scan}; use trace::TraceArgs; use verify::VerifyArgs; @@ -189,7 +189,7 @@ impl Cli { .to_str() .ok_or(anyhow!("file extension not recognized"))? { - "xml" => self.run_scxml(&model), + "xml" | "scxml" => self.run_scxml(&model), "jani" => self.run_jani(&model), "pml" | "prm" => self.run_promela(&model), _ => bail!("unsupported file format"), @@ -211,8 +211,7 @@ impl Cli { validate_properties(&args.properties, &scxml_model.guarantees)?; // Reorder properties as they appear in the model args.properties = scxml_model.guarantees.clone(); - run_verification::(model, &args, progress, json, &scan_def) - .print(json); + run_verification::<_>(model, &args, progress, json, &scan_def).print(json); } Commands::Validate => { let (_scan, _scxml_model) = load(&self.model, &[], true)?; @@ -224,9 +223,8 @@ impl Cli { validate_properties(&args.properties, &scxml_model.guarantees)?; // Reorder properties as they appear in the model args.properties = scxml_model.guarantees.clone(); - let scxml_model = Arc::new(scxml_model); - let tracer = TracePrinter::new(&scxml_model); - args.trace::(&scan_def, tracer); + let path = new_traces_dir(); + args.trace::<_, TracePrinter>(&scan_def, path, &scxml_model); println!("trace computation for model '{model}' completed"); } } @@ -248,8 +246,7 @@ impl Cli { validate_properties(&args.properties, &jani_model.guarantees)?; // Reorder properties as they appear in the model args.properties = jani_model.guarantees.clone(); - run_verification::(model, &args, progress, json, &scan) - .print(json); + run_verification::<_>(model, &args, progress, json, &scan).print(json); } Commands::Validate => { let (_scan, _jani_model) = load(&self.model, &[])?; @@ -258,9 +255,8 @@ impl Cli { Commands::Trace(args) => { args.validate()?; let (scan, jani_model) = load(&self.model, &[])?; - let jani_model = Arc::new(jani_model); - let tracer = TracePrinter::new(jani_model); - args.trace::(&scan, tracer); + let path = new_traces_dir(); + args.trace::<_, TracePrinter>(&scan, path, &jani_model); println!("trace computation for model '{model}' completed"); } } @@ -279,8 +275,7 @@ impl Cli { args.validate()?; let properties = args.properties.clone(); let (scan, _promela_model) = load(&self.model, &properties, args.all)?; - run_verification::(model, &args, progress, json, &scan) - .print(json); + run_verification::<_>(model, &args, progress, json, &scan).print(json); } Commands::Validate => { let (_scan, _jani_model) = load(&self.model, &[], true)?; @@ -306,17 +301,15 @@ fn validate_properties(props: &[String], all_props: &[String]) -> anyhow::Result } } -fn run_verification<'a, Ts, O>( +fn run_verification<'a, O>( model: &str, args: &VerifyArgs, progress: Option, json: bool, - scan: &'a Scan, + scan: &'a Scan, ) -> Report where - Ts: 'a + TransitionSystemGenerator + Sync, O: 'a + Oracle + Clone + Sync, - Ts::Ts<'a>: Clone + Sync, { if !json { println!( @@ -327,20 +320,35 @@ where if let Some(bar) = progress { std::thread::scope(|s| { s.spawn(|| { - bar.print_progress_bar::( + bar.print_progress_bar::( args.confidence, args.precision, &args.properties, scan, ); }); - args.verify::(model.to_owned(), scan) + args.verify::(model.to_owned(), scan) }) } else { - args.verify::(model.to_owned(), scan) + args.verify::(model.to_owned(), scan) } } +fn new_traces_dir() -> std::path::PathBuf { + const FOLDER: &str = "traces"; + + let mut path = current_dir().expect("current dir"); + for i in 0.. { + path.push(format!("{}_{i:02}", FOLDER)); + if std::fs::exists(&path).is_ok_and(|exists| !exists) { + break; + } else { + assert!(path.pop()); + } + } + path +} + // From Clap tutorial #[test] fn verify_cli() { diff --git a/src/progress.rs b/src/progress.rs index a76adb4..c637923 100644 --- a/src/progress.rs +++ b/src/progress.rs @@ -1,6 +1,6 @@ use clap::ValueEnum; use indicatif::{MultiProgress, ProgressBar, ProgressStyle}; -use scan_core::{Oracle, Scan, TransitionSystemGenerator, adaptive_bound, okamoto_bound}; +use scan_core::{Oracle, Scan, adaptive_bound, okamoto_bound}; /// Verification progress bar #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum)] @@ -13,12 +13,12 @@ pub(crate) enum Bar { } impl Bar { - pub(crate) fn print_progress_bar( + pub(crate) fn print_progress_bar( &self, confidence: f64, precision: f64, guarantees: &[String], - scan: &Scan, + scan: &Scan, ) { const FINE_BAR: &str = "█▉▊▋▌▍▎▏ "; const ASCII_BAR: &str = "#--"; @@ -75,11 +75,10 @@ impl Bar { } // Spinner + // Trailing spaces because bar does not overwrite after itself let spinner_style = - ProgressStyle::with_template("{elapsed_precise} {msg}: {pos}/{len} ({eta})").unwrap(); - // if let Bar::Plain = self { - // spinner_style = spinner_style.tick_chars(ASCII_SPINNER); - // } + ProgressStyle::with_template("{elapsed_precise} {msg}: {pos}/{len} ({eta}) ") + .unwrap(); let spinner = ProgressBar::new(0) .with_style(spinner_style) .with_message("verification progress"); diff --git a/src/trace.rs b/src/trace.rs index 2f098f0..e9c7564 100644 --- a/src/trace.rs +++ b/src/trace.rs @@ -1,6 +1,8 @@ +use std::path::PathBuf; + use anyhow::anyhow; use clap::Parser; -use scan_core::{Oracle, Scan, Time, Tracer, TransitionSystem, TransitionSystemGenerator}; +use scan_core::{Oracle, Scan, Time, Tracer}; const ALL_PROPS_ERR: &str = "the --all flag is incompatible with individually-specified properties.\n @@ -23,7 +25,7 @@ pub(crate) struct TraceArgs { #[arg(long, default_value_t = 1)] pub(crate) traces: usize, /// Max duration of execution (in model-time). - #[arg(short, long, default_value_t = 10000)] + #[arg(short, long, default_value_t = 0)] pub(crate) duration: Time, /// Run the model execution on a single thread. /// @@ -49,18 +51,16 @@ impl TraceArgs { } } - pub(crate) fn trace<'a, D, Od, Tr>(&self, scan: &'a Scan, tracer: Tr) + pub(crate) fn trace<'a, Od, Tr>(&self, scan: &'a Scan, path: PathBuf, model: &Tr::ModelData) where - D: TransitionSystemGenerator + Sync + 'a, Od: Oracle + Sync + 'a, - Tr: Clone - + Sync - + Tracer<<::Ts<'a> as TransitionSystem>::Event>, + Tr: Tracer, + Tr::ModelData: Sync, { if self.single_thread { - scan.traces::(self.traces, tracer, self.duration); + scan.traces::(self.traces, self.duration, path, model); } else { - scan.par_traces::(self.traces, tracer, self.duration); + scan.par_traces::(self.traces, self.duration, path, model); } } } diff --git a/src/verify.rs b/src/verify.rs index d9db21f..1ea9245 100644 --- a/src/verify.rs +++ b/src/verify.rs @@ -1,6 +1,6 @@ use anyhow::anyhow; use clap::Parser; -use scan_core::{Oracle, Scan, Time, TransitionSystemGenerator}; +use scan_core::{Oracle, Scan, Time}; use super::report::Report; @@ -50,7 +50,7 @@ pub(crate) struct VerifyArgs { pub(crate) precision: f64, /// Max duration of execution (in model-time), /// to prevent infinite executions. - #[arg(short, long, default_value_t = 10000)] + #[arg(short, long, default_value_t = 0)] pub(crate) duration: Time, /// Run the verification on a single thread. /// @@ -80,9 +80,8 @@ impl VerifyArgs { } } - pub(crate) fn verify<'a, Ts, O>(&self, model: String, scan: &'a Scan) -> Report + pub(crate) fn verify<'a, O>(&self, model: String, scan: &'a Scan) -> Report where - Ts: TransitionSystemGenerator + Sync + 'a, O: Oracle + Sync + 'a, { if self.single_thread {