{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:54:15Z","timestamp":1757310855999,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030628215"},{"type":"electronic","value":"9783030628222"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-62822-2_8","type":"book-chapter","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T21:04:28Z","timestamp":1604869468000},"page":"124-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic Model Checking with Sentential Decision Diagrams"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1825-0097","authenticated-orcid":false,"given":"Lieuwe","family":"Vinkhuijzen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2433-4174","authenticated-orcid":false,"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,9]]},"reference":[{"key":"8_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"8","key":"8_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR3","unstructured":"McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem. Ph.d. thesis. UMI No. GAX92-24209 (1992)"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Van den Broeck, G., Darwiche, A.: On the role of canonicity in knowledge compilation. In: Twenty-Ninth AAAI Conference on Artificial Intelligence (2015)","DOI":"10.1609\/aaai.v29i1.9423"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Livshits, B., et al.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44\u201346 (2015)","DOI":"10.1145\/2644805"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Requeno, J.I., Colom, J.M.: Compact representation of biological sequences using set decision diagrams. In: Rocha, M., Luscombe, N., Fdez-Riverola, F., Rodr\u00edguez, J., (eds.) 6th International Conference on Practical Applications of Computational Biology & Bioinformatics, vol. 154, pp. 231\u2013239. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28839-5_27","DOI":"10.1007\/978-3-642-28839-5_27"},{"key":"8_CR11","unstructured":"Bergman, D., Cire, A.A., van Hoeve, W.-J., Hooker, J.N.: Discrete optimization with decision diagrams. INFORMS J. Comput. 28(1), 47\u201366 (2016)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Niemann, P., Zulehner, A., Drechsler, R., Wille, R.: Overcoming the trade-off between accuracy and compactness in decision diagrams for quantum computation. IEEE Trans. Comput. Aid. Des. Integr. Circuits Syst. (2020)","DOI":"10.1109\/TCAD.2020.2977603"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Minato, S.: Zero-suppressed BDDs for set manipulation in combinatorial problems. In: 30th ACM\/IEEE Design Automation Conference, pp. 272\u2013277. IEEE (1993)","DOI":"10.1145\/157485.164890"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"van Dijk, T., Wille, R., Meolic, R.: Tagged BDDs: combining reduction rules from different decision diagram types. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, pp. 108\u2013115. FMCAD Inc. (2017)","DOI":"10.23919\/FMCAD.2017.8102248"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-319-89960-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2018","unstructured":"Bryant, R.E.: Chain reduction for binary and zero-suppressed decision diagrams. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 81\u201398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_5"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-17465-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Babar","year":"2019","unstructured":"Babar, J., Jiang, C., Ciardo, G., Miner, A.: Binary decision diagrams with edge-specified reductions. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 303\u2013318. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_17"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Nishino, M., Yasuda, N., Minato, S., Nagata, M.: Zero-suppressed sentential decision diagrams. In: Thirtieth AAAI Conference on Artificial Intelligence (2016)","DOI":"10.1609\/aaai.v30i1.10114"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Fang, L., Fang, B., Wan, H., Zheng, Z., Chang, L., Yu, Q.: Tagged sentential decision diagrams: combining standard and zero-suppressed compression and trimming rules (2019)","DOI":"10.1109\/ICCAD45719.2019.8942114"},{"key":"8_CR19","unstructured":"Nakamura, K., Denzumi, S., Nishino, M.: Variable shift SDD: a more succinct sentential decision diagram. In: Faro, S., Cantone, D., (eds.) 18th International Symposium on Experimental Algorithms (SEA 2020), volume 160 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 22:1\u201322:13, Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"8_CR20","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence-Volume, vol. 2, pp. 819\u2013826. AAAI Press (2011)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Bova, S.: SDDs are exponentially more succinct than OBDDs. In: Thirtieth AAAI Conference on Artificial Intelligence (2016)","DOI":"10.1609\/aaai.v30i1.10107"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Choi, A., Darwiche, A.: Dynamic minimization of sentential decision diagrams. In: Twenty-Seventh AAAI Conference on Artificial Intelligence (2013)","DOI":"10.1609\/aaai.v27i1.8690"},{"key":"8_CR23","unstructured":"UCLA Automated Reasoning Group. The SDD package (2018). http:\/\/reasoning.cs.ucla.edu\/sdd\/"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Baranov\u00e1, Z., Barnat, J., Kejstov\u00e1, K., Ku\u010dera, T., Lauko, H., Mr\u00e1zek, J., Ro\u010dkai, P., \u0160till, V.: Model Checking of C and C++ with DIVINE 4. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201\u2013207. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14","DOI":"10.1007\/978-3-319-68167-2_14"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-662-58381-4_9","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XIII","author":"F Kordon","year":"2018","unstructured":"Kordon, F., et al.: MCC\u20192017 \u2013 the seventh model checking contest. In: Koutny, M., Kristensen, L.M., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XIII. LNCS, vol. 11090, pp. 181\u2013209. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58381-4_9"},{"key":"8_CR26","first-page":"279","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE TSE 23, 279\u2013295 (1997)","journal-title":"IEEE TSE"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.L The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"issue":"3","key":"8_CR29","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-13338-6_16","volume-title":"Hardware and Software: Verification and Testing","author":"J Meijer","year":"2014","unstructured":"Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 204\u2013219. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_16"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-40648-0_20","volume-title":"NASA Formal Methods","author":"J Meijer","year":"2016","unstructured":"Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 255\u2013271. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Cuthill, E., McKee, J.: Reducing the bandwidth of sparse symmetric matrices. In: Proceedings of the 1969 24th National Conference, pp. 157\u2013172. ACM (1969)","DOI":"10.1145\/800195.805928"},{"issue":"11","key":"8_CR33","doi-asserted-by":"publisher","first-page":"2651","DOI":"10.1002\/nme.1620281111","volume":"28","author":"SW Sloan","year":"1989","unstructured":"Sloan, S.W.: A fortran program for profile and wavefront reduction. Int. J. Numer. Meth. Eng. 28(11), 2651\u20132679 (1989)","journal-title":"Int. J. Numer. Meth. Eng."},{"key":"8_CR34","unstructured":"Aloul, F., Markov, I., Sakallah, K.: Mince: a static global variable-ordering for sat and BDD. In: International Workshop on Logic and Synthesis, pp. 1167\u20131172 (2001)"},{"key":"8_CR35","unstructured":"Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD\/MDD construction. University of California, Technical report (2008)"},{"key":"8_CR36","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11691372_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RI Siminiceanu","year":"2006","unstructured":"Siminiceanu, R.I., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 90\u2013104. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_6"},{"key":"8_CR38","unstructured":"Oztok, U., Darwiche, A.: CV-width: a new complexity parameter for CNFs. In: ECAI, pp. 675\u2013680 (2014)"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in AK-tree. SIAM J. Algebraic Discrete Methods 8(2), 277\u2013284 (1987)","DOI":"10.1137\/0608024"},{"key":"8_CR40","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1613\/jair.4030","volume":"49","author":"W Yu","year":"2014","unstructured":"Yu, W., Austrin, P., Pitassi, T., Liu, D.: Inapproximability of treewidth and related problems. J. Artif. Intell. Res. 49, 569\u2013600 (2014)","journal-title":"J. Artif. Intell. Res."},{"key":"8_CR41","unstructured":"Bodlaender, H.L.: A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput. 25(6), 1305\u20131317 (1996)"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_17"},{"key":"8_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-662-53401-4_12","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XI","author":"F Kordon","year":"2016","unstructured":"Kordon, F., et al.: MCC\u20192015 \u2013 the fifth model checking contest. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 262\u2013273. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53401-4_12"},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T van Dijk","year":"2015","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-62822-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,27]],"date-time":"2022-11-27T07:54:33Z","timestamp":1669535673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62822-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030628215","9783030628222"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62822-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"9 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lcs.ios.ac.cn\/setta2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}