{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T21:49:48Z","timestamp":1672523388509},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,5,16]],"date-time":"2012-05-16T00:00:00Z","timestamp":1337126400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1007\/s10703-012-0160-6","type":"journal-article","created":{"date-parts":[[2012,5,15]],"date-time":"2012-05-15T16:52:38Z","timestamp":1337100758000},"page":"129-177","source":"Crossref","is-referenced-by-count":1,"title":["Deadlock-freedom in component systems with architectural constraints"],"prefix":"10.1007","volume":"41","author":[{"given":"Moritz","family":"Martens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mila","family":"Majster-Cederbaum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,5,16]]},"reference":[{"key":"160_CR1","unstructured":"Enterprise JavaBeans. See: http:\/\/java.sun.com\/products\/ejb"},{"key":"160_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-642-04420-5_6","volume-title":"Proceedings of LIX colloquium reachability problems\u201909","author":"PA Abdulla","year":"2009","unstructured":"Abdulla PA, Delzanno G, Rezine A (2009) Automatic verification of Directory-Based consistency protocols. In: Proceedings of LIX colloquium reachability problems\u201909. LNCS, vol\u00a05797. Springer, Berlin, pp 36\u201350"},{"key":"160_CR3","doi-asserted-by":"crossref","unstructured":"Apt KR, Francez N, de Roever WP (1980) A proof system for communicating sequential processes. ACM Trans Program Lang Syst 2(3). doi: 10.1145\/357103.357110","DOI":"10.1145\/357103.357110"},{"key":"160_CR4","series-title":"LNCS","first-page":"465","volume-title":"Proceedings of VMCAI\u201905","author":"PC Attie","year":"2005","unstructured":"Attie PC, Chockler H (2005) Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: Proceedings of VMCAI\u201905. LNCS, vol\u00a03385, pp 465\u2013481"},{"issue":"1","key":"160_CR5","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"PC Attie","year":"1998","unstructured":"Attie PC, Emerson EA (1998) Synthesis of concurrent systems with many similar processes. ACM Trans Program Lang Syst 20(1):51\u2013115","journal-title":"ACM Trans Program Lang Syst"},{"issue":"4","key":"160_CR6","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1145\/48022.48023","volume":"10","author":"R-J Back","year":"1988","unstructured":"Back R-J, Kurki-Suonio R (1988) Distributed cooperation with action systems. ACM Trans Program Lang Syst 10(4):513\u2013554","journal-title":"ACM Trans Program Lang Syst"},{"key":"160_CR7","unstructured":"Badouel E, Benveniste A, Bozga M, Caillaud B, Constant O, Josko B, Ma Q, Passerone R, Skipper M (2007) SPEEDS Metamodel Syntax and Draft Semantics. Deliverable D2.1c"},{"key":"160_CR8","first-page":"3","volume-title":"Proceedings of SEFM\u201906","author":"A Basu","year":"2006","unstructured":"Basu A, Bozga M, Sifakis J (2006) Modeling heterogeneous real-time components in BIP. In: Proceedings of SEFM\u201906. IEEE Comput Soc, Los Alamitos, pp 3\u201312"},{"key":"160_CR9","series-title":"ENTCS","first-page":"75","volume-title":"Proceedings of FACS\u201905","author":"H Baumeister","year":"2006","unstructured":"Baumeister H, Hacklinger F, Hennicker R, Knapp A, Wirsing M (2006) A component model for architectural programming. In: Proceedings of FACS\u201905. ENTCS, vol\u00a0160. Elsevier, Amsterdam, pp 75\u201396"},{"key":"160_CR10","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1145\/606612.606614","volume":"11","author":"M Bernardo","year":"2002","unstructured":"Bernardo M, Ciancarini P, Donatiello L (2002) Architecting families of software systems with process algebras. ACM Trans Softw Eng Methodol 11:386\u2013426","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"160_CR11","unstructured":"Bozga M, Constant O, Josko B, Ma Q, Skipper M (2007) SPEEDS Metamodel Syntax and Static Semantics. Deliverable D2.1b"},{"key":"160_CR12","first-page":"40","volume-title":"Proceedings of DAC\u201990","author":"KS Brace","year":"1990","unstructured":"Brace KS, Rudell RL, Bryant RE (1990) Efficient implementation of a BDD package. In: Proceedings of DAC\u201990. IEEE Comput Soc, Los Alamitos, pp 40\u201345"},{"issue":"4","key":"160_CR13","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01784721","volume":"4","author":"S Brookes","year":"1991","unstructured":"Brookes S, Roscoe A (1991) Deadlock analysis in networks of communicating processes. Distrib Comput 4(4):209\u2013230","journal-title":"Distrib Comput"},{"issue":"8","key":"160_CR14","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-Based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"160_CR15","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u2013318","journal-title":"ACM Comput Surv"},{"key":"160_CR16","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1145\/24039.24050","volume":"9","author":"A Charlesworth","year":"1987","unstructured":"Charlesworth A (1987) The multiway rendezvous. ACM Trans Program Lang Syst 9:350\u2013366","journal-title":"ACM Trans Program Lang Syst"},{"key":"160_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of logics of programs\u201981","author":"EM Clarke","year":"1982","unstructured":"Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of logics of programs\u201981. LNCS, vol\u00a0131. Springer, Berlin, pp 52\u201371"},{"key":"160_CR18","first-page":"450","volume-title":"CAV\u201993","author":"EM Clarke","year":"1993","unstructured":"Clarke EM, Filkorn T, Jha S (1993) Exploiting symmetry in temporal logic model checking. In: CAV\u201993, pp 450\u2013462"},{"issue":"2","key":"160_CR19","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of Finite-State concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"key":"160_CR20","first-page":"353","volume-title":"Proceedings of LICS\u201989","author":"EM Clarke","year":"1989","unstructured":"Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: Proceedings of LICS\u201989. IEEE Comput Soc, Los Alamitos, pp 353\u2013362"},{"issue":"4","key":"160_CR21","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1145\/242223.242252","volume":"28","author":"R Cleaveland","year":"1996","unstructured":"Cleaveland R, Smolka SA (1996) Strategic directions in concurrency research. ACM Comput Surv 28(4):607\u2013625","journal-title":"ACM Comput Surv"},{"key":"160_CR22","first-page":"238","volume-title":"Proceedings of POPL\u201977","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL\u201977, pp 238\u2013252"},{"key":"160_CR23","first-page":"109","volume-title":"Proceedings of FSE\u201901","author":"L Alfaro de","year":"2001","unstructured":"de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of FSE\u201901, pp 109\u2013120"},{"key":"160_CR24","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-1-4612-5695-3","volume-title":"Selected writings on computing","author":"E Dijkstra","year":"1982","unstructured":"Dijkstra E, Scholten C (1982) A class of simple communication patterns, EWD643. In: Dijkstra E (ed) Selected writings on computing. Springer, Berlin, pp 334\u2013337"},{"key":"160_CR25","series-title":"LNCS","first-page":"463","volume-title":"Proceedings of CAV\u201993","author":"EA Emerson","year":"1993","unstructured":"Emerson EA, Sistla AP (1993) Symmetry and model checking. In: Proceedings of CAV\u201993. LNCS, vol\u00a0697. Springer, Berlin, pp 463\u2013478"},{"issue":"11","key":"160_CR26","doi-asserted-by":"crossref","first-page":"1417","DOI":"10.1109\/32.41333","volume":"15","author":"M Evangelist","year":"1989","unstructured":"Evangelist M, Francez N, Katz S (1989) Multiparty interactions for interprocess communication and synchronization. IEEE Trans Softw Eng 15(11):1417\u20131426","journal-title":"IEEE Trans Softw Eng"},{"key":"160_CR27","series-title":"LNCS","first-page":"176","volume-title":"Proceedings of CAV\u201990","author":"P Godefroid","year":"1990","unstructured":"Godefroid P (1990) Using partial orders to improve automatic verification methods. In: Proceedings of CAV\u201990. LNCS, vol\u00a0531. Springer, Berlin, pp 176\u2013185"},{"issue":"2","key":"160_CR28","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P Godefroid","year":"1993","unstructured":"Godefroid P, Wolper P (1993) Using partial orders for the efficient verification of deadlock freedom and safety properties. Form Methods Syst Des 2(2):149\u2013164. ISSN 0925-9856","journal-title":"Form Methods Syst Des"},{"key":"160_CR29","unstructured":"Go\u00dfB (2010) A BDD-Based algorithm for checking Deadlock-Freedom in Tree-Like component systems. Bachelor thesis, University of Mannheim"},{"key":"160_CR30","unstructured":"G\u00f6ssler G (2006) Component-based design of heterogeneous reactive systems in prometheus. Technical report 6057, INRIA"},{"key":"160_CR31","series-title":"LNCS","first-page":"420","volume-title":"Proceedings of FSTTCS\u201903","author":"G G\u00f6ssler","year":"2003","unstructured":"G\u00f6ssler G, Sifakis J (2003) Component-Based construction of Deadlock-Free systems. In: Proceedings of FSTTCS\u201903. LNCS, vol\u00a02914, pp 420\u2013433"},{"key":"160_CR32","series-title":"LNCS","first-page":"443","volume-title":"Proceedings of FMCO\u201902","author":"G G\u00f6ssler","year":"2003","unstructured":"G\u00f6ssler G, Sifakis J (2003) Composition for Component-Based modeling. In: Proceedings of FMCO\u201902. LNCS, vol\u00a02852, pp 443\u2013466"},{"issue":"1\u20133","key":"160_CR33","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/j.scico.2004.05.014","volume":"55","author":"G G\u00f6ssler","year":"2005","unstructured":"G\u00f6ssler G, Sifakis J (2005) Composition for component-based modeling. Sci Comput Program 55(1\u20133):161\u2013183","journal-title":"Sci Comput Program"},{"key":"160_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-71322-7_10","volume-title":"Program analysis and computation, theory and practice","author":"G G\u00f6ssler","year":"2007","unstructured":"G\u00f6ssler G, Graf S, Majster-Cederbaum M, Martens M, Sifakis J (2007) Ensuring properties of interaction systems. In: Program analysis and computation, theory and practice. LNCS, vol\u00a04444, pp 201\u2013224"},{"key":"160_CR35","series-title":"LNCS","first-page":"295","volume-title":"Proceedings of SOFSEM 07","author":"G G\u00f6ssler","year":"2007","unstructured":"G\u00f6ssler G, Graf S, Majster-Cederbaum M, Martens M, Sifakis J (2007) An approach to modelling and verification of component based systems. In: Proceedings of SOFSEM 07. LNCS, vol\u00a04362, pp 295\u2013308"},{"key":"160_CR36","series-title":"ENTCS","first-page":"1","volume-title":"Proceedings of FACS\u201908","author":"R Hennicker","year":"2008","unstructured":"Hennicker R, Janisch S, Knapp A (2008) On the observable behaviour of composite components. In: Canal C, Pasareanu C (eds) Proceedings of FACS\u201908. ENTCS. Elsevier, Amsterdam, pp 1\u201326"},{"key":"160_CR37","series-title":"Series in computer science","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Series in computer science. Prentice Hall, New York"},{"key":"160_CR38","series-title":"LNCS","first-page":"60","volume-title":"Proceedings of FASE\u201901","author":"P Inverardi","year":"2001","unstructured":"Inverardi P, Uchitel S (2001) Proving deadlock freedom in component-based programming. In: Proceedings of FASE\u201901. LNCS, vol\u00a02029, pp 60\u201375"},{"issue":"3","key":"160_CR39","doi-asserted-by":"crossref","first-page":"954","DOI":"10.1145\/177492.177739","volume":"16","author":"Y-J Joung","year":"1994","unstructured":"Joung Y-J, Smolka SA (1994) Coordinating first-order multiparty interactions. ACM Trans Program Lang Syst 16(3):954\u2013985","journal-title":"ACM Trans Program Lang Syst"},{"key":"160_CR40","doi-asserted-by":"crossref","unstructured":"Kanellakis PC, Smolka SA (1990) CCS expressions, finite state processes, and three problems of equivalence. Inf Comput 86(1). doi: 10.1016\/0890-5401(90)90025-D","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"160_CR41","series-title":"LNCS","volume-title":"Proceedings of FSEN\u201911","author":"C Lambertz","year":"2011","unstructured":"Lambertz C, Majster-Cederbaum M (2011) Analyzing component-based systems on the basis of architectural constraints. In: Proceedings of FSEN\u201911. LNCS, vol\u00a07141. Springer, Berlin"},{"key":"160_CR42","unstructured":"Lambertz C, Majster-Cederbaum M (2011, submitted) Analysis and complexity of Component-Based software architectures"},{"issue":"10","key":"160_CR43","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1109\/TSE.2007.70726","volume":"33","author":"K-K Lau","year":"2007","unstructured":"Lau K-K, Wang Z (2007) Software component models. IEEE Trans Softw Eng 33(10):709\u2013724","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"160_CR44","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch NA, Tuttle MR (1989) An introduction to input\/output automata. Quart - Cent Wiskd Inform 2(3):219\u2013246","journal-title":"Quart - Cent Wiskd Inform"},{"key":"160_CR45","series-title":"LNCS","first-page":"352","volume-title":"Proceedings of SOFSEM\u201908","author":"M Majster-Cederbaum","year":"2008","unstructured":"Majster-Cederbaum M, Minnameier C (2008) Deriving complexity results for interaction systems from 1-safe petri nets. In: Proceedings of SOFSEM\u201908. LNCS, vol\u00a04910. Springer, Berlin, pp 352\u2013363"},{"key":"160_CR46","series-title":"LNCS","first-page":"216","volume-title":"Proceedings of ICTAC\u201908","author":"M Majster-Cederbaum","year":"2008","unstructured":"Majster-Cederbaum M, Minnameier C (2008) Everything is PSPACE-complete in interaction systems. In: Proceedings of ICTAC\u201908. LNCS, vol\u00a05160. Springer, Berlin, pp 216\u2013227"},{"key":"160_CR47","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-642-04420-5_18","volume-title":"Proceedings of the LIX colloquium on reachability problems\u201909","author":"M Majster-Cederbaum","year":"2009","unstructured":"Majster-Cederbaum M, Minnameier C (2009) Cross-Checking\u2014enhanced over-approximation of the reachable global state space of component-based systems. In: Proceedings of the LIX colloquium on reachability problems\u201909. LNCS, vol\u00a05797. Springer, Berlin, pp 189\u2013202"},{"key":"160_CR48","series-title":"LNCS","first-page":"888","volume-title":"Proceedings of SOFSEM\u201907","author":"M Majster-Cederbaum","year":"2007","unstructured":"Majster-Cederbaum M, Martens M, Minnameier C (2007) A polynomial-time checkable sufficient condition for Deadlock-Freedom of component based systems. In: Proceedings of SOFSEM\u201907. LNCS, vol\u00a04362, pp 888\u2013899"},{"key":"160_CR49","unstructured":"Martens M (2010) A BDD-based algorithm for deadlock-freedom in tree-Like component architectures. See: http:\/\/pi2\/BDDTooL\/index.html (Password can be provided upon request)"},{"key":"160_CR50","first-page":"199","volume-title":"Proceedings of EMSOFT\u201908","author":"M Martens","year":"2008","unstructured":"Martens M, Majster-Cederbaum M (2008) Compositional analysis of tree-like component architecures. In: Proceedings of EMSOFT\u201908. ACM, New York , pp 199\u2013206"},{"key":"160_CR51","first-page":"225","volume-title":"Proceedings of TASE\u201909","author":"M Martens","year":"2009","unstructured":"Martens M, Majster-Cederbaum M (2009) Using architectural constraints for deadlock-freedom of component systems with multiway cooperation. In: Proceedings of TASE\u201909. IEEE Comput. Soc., Los Alamitos, pp 225\u2013232. IEEE Conference Publishing Services"},{"key":"160_CR52","volume-title":"Applying enterprise JavaBeans 2.1: component-based development for the J2EE platform","author":"V Matena","year":"2003","unstructured":"Matena V, Krishnan S, DeMichiel L, Stearns B (2003) Applying enterprise JavaBeans 2.1: component-based development for the J2EE platform, 2nd edn. Addison-Wesley, Reading","edition":"2"},{"key":"160_CR53","volume-title":"Software ecosystem\u2014understanding an indispensable technology and industry","author":"D Messerschmitt","year":"2003","unstructured":"Messerschmitt D, Szyperski C (2003) Software ecosystem\u2014understanding an indispensable technology and industry. MIT Press, Cambridge"},{"key":"160_CR54","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall, New York"},{"key":"160_CR55","volume-title":"The art of software testing","author":"GJ Myers","year":"2004","unstructured":"Myers GJ (2004) The art of software testing, 2nd edn. Wiley, New York","edition":"2"},{"key":"160_CR56","doi-asserted-by":"crossref","unstructured":"Paige R, Tarjan RE (1987) Three partition refinement algorithms. SIAM J Comput 16(6). doi: 10.1137\/0216062","DOI":"10.1137\/0216062"},{"key":"160_CR57","series-title":"ENTCS","first-page":"139","volume-title":"Proceedings of FACS\u201906","author":"P Parizek","year":"2007","unstructured":"Parizek P, Plasil F (2007) Modeling environment for component model checking from hierarchical architecture. In: Proceedings of FACS\u201906. ENTCS, vol\u00a0182. Elsevier, Amsterdam, pp 139\u2013153"},{"key":"160_CR58","series-title":"LNCS","first-page":"409","volume-title":"Proceedings of CAV\u201993","author":"D Peled","year":"1993","unstructured":"Peled D (1993) All from one, one for all: on model checking using representatives. In: Proceedings of CAV\u201993. LNCS, vol\u00a0697. Springer, Berlin, pp 409\u2013423"},{"key":"160_CR59","first-page":"46","volume-title":"Proceedings of FOCS\u201977","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of FOCS\u201977. IEEE Press, New York, pp 46\u201357"},{"key":"160_CR60","unstructured":"Semmelrock N (2010) A BDD tool for interaction systems. See: http:\/\/pi2\/BDDTooL\/index.html (Password can be provided upon request)"},{"key":"160_CR61","volume-title":"Proceedings of FACS\u201909","author":"N Semmelrock","year":"2009","unstructured":"Semmelrock N, Majster-Cederbaum M (2009) Reachability in tree-like component systems is PSPACE-complete. In: Proceedings of FACS\u201909. doi: 10.1016\/j.entcs.2010.05.012 . Accepted for publication"},{"key":"160_CR62","volume-title":"Software engineering","author":"I Sommerville","year":"2007","unstructured":"Sommerville I (2007) Software engineering, 8th edn. Pearson Education, Upper Saddle River. Chapters\u00a011 and\u00a012","edition":"8"},{"key":"160_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-3-642-04420-5_5","volume-title":"Proceedings of LIX colloquium reachability Problems\u201909","author":"MY Vardi","year":"2009","unstructured":"Vardi MY (2009) Model checking as a reachability problem. In: Proceedings of LIX colloquium reachability Problems\u201909. LNCS, vol\u00a05797. Springer, Berlin, p\u00a035. Key note talk"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0160-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0160-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0160-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:52Z","timestamp":1559253952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0160-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,16]]},"references-count":63,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["160"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0160-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,16]]}}}