{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:36Z","timestamp":1776373536846,"version":"3.51.2"},"reference-count":126,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2008,12,11]],"date-time":"2008-12-11T00:00:00Z","timestamp":1228953600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif &amp; Rel"],"published-print":{"date-parts":[[2009,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>About a decade after the initial proposal to use model checkers for the generation of test cases we take a look at the results in this field of research. Model checkers are formal verification tools, capable of providing counterexamples to violated properties. Normally, these counterexamples are meant to guide an analyst when searching for the root cause of a property violation. They are, however, also very useful as test cases. Many different approaches have been presented, many problems have been solved, yet many issues remain. This survey paper reviews the state of the art in testing with model checkers. Copyright \u00a9 2008 John Wiley &amp; Sons, Ltd.<\/jats:p>","DOI":"10.1002\/stvr.402","type":"journal-article","created":{"date-parts":[[2009,8,27]],"date-time":"2009-08-27T16:11:30Z","timestamp":1251389490000},"page":"215-261","source":"Crossref","is-referenced-by-count":143,"title":["Testing with model checkers: a survey"],"prefix":"10.1002","volume":"19","author":[{"given":"Gordon","family":"Fraser","sequence":"first","affiliation":[]},{"given":"Franz","family":"Wotawa","sequence":"additional","affiliation":[]},{"given":"Paul E.","family":"Ammann","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2008,12,11]]},"reference":[{"key":"e_1_2_1_2_2","unstructured":"CallahanJ SchneiderF EasterbrookS.Automated software testing using model\u2010checking. Proceedings 1996 SPIN Workshop August 1996. Also WVU Technical Report NASA\u2010IVV\u201096\u2010022."},{"key":"e_1_2_1_3_2","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97)","author":"Engels A","year":"1997"},{"key":"e_1_2_1_4_2","unstructured":"UttingM PretschnerA LegeardB.A taxonomy of model\u2010based testing. Technical Report No. 04\/2006 Department of Computer Science The University of Waikato New Zealand April2006."},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318622"},{"key":"e_1_2_1_6_2","first-page":"332","volume-title":"Proceedings of the 1st IEEE Symposium on Logic in Computer Science (LICS'86)","author":"Vardi MY","year":"1986"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"CAV '99: Proceedings of the 11th International Conference on Computer Aided Verification","author":"Cimatti A","year":"1999"},{"key":"e_1_2_1_10_2","unstructured":"McMillanKL.The SMV system. Technical Report CMU\u2010CS\u201092\u2010131 Carnegie\u2010Mellon University 1992."},{"key":"e_1_2_1_11_2","first-page":"46","volume-title":"Eighteenth Annual Symposium on Foundations of Computer Science","author":"Pnueli A","year":"1977"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802190"},{"key":"e_1_2_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_1_17_2"},{"key":"e_1_2_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53479-2_17"},{"key":"e_1_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1995.249985"},{"key":"e_1_2_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_1_22_2"},{"key":"e_1_2_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_24_2","doi-asserted-by":"publisher","DOI":"10.1002\/1099-1689(200012)10:4<229::AID-STVR213>3.0.CO;2-O"},{"key":"e_1_2_1_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39910-0_9"},{"key":"e_1_2_1_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029814"},{"key":"e_1_2_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1291535.1291543"},{"key":"e_1_2_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2_17"},{"key":"e_1_2_1_31_2","first-page":"146","volume-title":"ESEC\/FSE'99: 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"Gargantini A","year":"1999"},{"key":"e_1_2_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/b137241"},{"key":"e_1_2_1_33_2","unstructured":"HongHS LeeI.Automatic test generation from specifications for control\u2010flow and data\u2010flow coverage criteria. Proceedings of Monterey Workshop Naval Postgraduate School Monterey CA June 2001;230\u2013246."},{"key":"e_1_2_1_34_2","first-page":"300","volume-title":"Proceedings of the 8th IEEE International Symposium on Object\u2010oriented Real\u2010time Distributed Computing","author":"Huan H","year":"2005"},{"key":"e_1_2_1_35_2","unstructured":"Garcia\u2010FanjulJ TuyaJ de la RivaC.Generating test cases specifications for BPEL compositions of web services using SPIN. Proceedings of the International Workshop on Web Services Modeling and Testing (WS\u2010MaTe 2006) Palermo Italy 2006;83\u201394."},{"key":"e_1_2_1_36_2","unstructured":"TanL SokolskyO LeeI.Specification\u2010based testing with linear temporal logic. Proceedings of IEEE International Conference on Information Reuse and Integration (IRI'04) Las Vegas U.S.A. 2004;493\u2013498."},{"key":"e_1_2_1_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.1998.730569"},{"key":"e_1_2_1_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809163"},{"key":"e_1_2_1_39_2","doi-asserted-by":"publisher","DOI":"10.1002\/0471028959.sof307"},{"key":"e_1_2_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343384"},{"issue":"11","key":"e_1_2_1_41_2","first-page":"1050","article-title":"ASM\u2010based testing: Coverage criteria and automatic test sequence","volume":"7","author":"Gargantini A","year":"2001","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36498-6_15"},{"key":"e_1_2_1_43_2","unstructured":"HeimdahlMPE RayadurgamS VisserW.Specification centered testing. Proceedings of the Second International Workshop on Automated Program Analysis Testing and Verification Toronto Canada May 2001."},{"key":"e_1_2_1_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2001.922409"},{"key":"e_1_2_1_45_2","unstructured":"RayadurgamS HeimdahlMPE.Coverage based test\u2010case generation using model checkers. Technical Report 01\u2010005 University of Minnesota Minneapolis 2001."},{"key":"e_1_2_1_46_2","isbn-type":"print","volume-title":"HASE '01: The 6th IEEE International Symposium on High\u2010Assurance Systems Engineering","author":"Rayadurgam S","year":"2001","ISBN":"https:\/\/id.crossref.org\/isbn\/0769512755"},{"key":"e_1_2_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/318773.318940"},{"key":"e_1_2_1_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2003.1251034"},{"key":"e_1_2_1_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.1999.802856"},{"key":"e_1_2_1_50_2","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1994.0025"},{"key":"e_1_2_1_51_2","doi-asserted-by":"crossref","unstructured":"RayadurgamS HeimdahlMPE.Generating MC\/DC adequate test sequences through model checking. Proceedings of the 28th Annual NASA Goddard Software Engineering Workshop Greenbelt MD 2003;91\u201396.","DOI":"10.1109\/SEW.2003.1270730"},{"key":"e_1_2_1_52_2","unstructured":"AmmannP BlackPE DingW.Model checkers in software testing. Technical Report NIST\u2010IR 6777 National Institute of Standards and Technology 2002."},{"key":"e_1_2_1_53_2","doi-asserted-by":"publisher","DOI":"10.1137\/0107041"},{"key":"e_1_2_1_54_2","first-page":"291","volume-title":"ZB '02: Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B","author":"Vilkomir SA","year":"2002"},{"key":"e_1_2_1_55_2","series-title":"Lecture Notes in Computer Science","first-page":"151","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002","author":"Hong HS","year":"2002"},{"key":"e_1_2_1_56_2","volume-title":"ICSE '03: Proceedings of the 25th International Conference on Software Engineering","author":"Hong HS","year":"2003"},{"key":"e_1_2_1_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.232226"},{"key":"e_1_2_1_58_2","series-title":"Lecture Notes in Computer Science","first-page":"23","volume-title":"Testing of Communicating Systems","author":"Hong HS","year":"2002"},{"key":"e_1_2_1_59_2","unstructured":"HongHS LeeI SokolskyO ChaSD.Automatic test generation from statecharts using model checking. Technical Report MS\u2010CIS\u201001\u201007 2001."},{"key":"e_1_2_1_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEW.2006.26"},{"key":"e_1_2_1_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978\u20103\u2010540\u201079124\u20109\u20106"},{"key":"e_1_2_1_62_2","unstructured":"CallahanJR EasterbrookSM MontgomeryTL.Generating test oracles via model checking. Technical Report NASA\/WVU Software Research Lab 1998."},{"key":"e_1_2_1_63_2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification","author":"Beer I","year":"1997"},{"key":"e_1_2_1_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_8"},{"key":"e_1_2_1_65_2","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification","author":"Purandare M","year":"2002"},{"key":"e_1_2_1_66_2","volume-title":"ISSTA'06: Proceedings of the 2006 International Symposium on Software Testing and Analysis","author":"Whalen MW","year":"2006"},{"key":"e_1_2_1_67_2","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/C-M.1978.218136","article-title":"Hints on test data selection: Help for the practicing programmer","volume":"11","author":"DeMillo RA","year":"1978","journal-title":"Computer"},{"key":"e_1_2_1_68_2","unstructured":"AcreeAT BuddTA DeMilloRA LiptonRJ SaywardFG.Mutation analysis. Technical Report School of Information and Computer Science Georgia Institute of Technology Atlanta GA 1979."},{"key":"e_1_2_1_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/0096\u20100551(85)90011\u20106"},{"key":"e_1_2_1_70_2","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.1999.809499"},{"key":"e_1_2_1_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2003.1254388"},{"key":"e_1_2_1_72_2","volume-title":"Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE'00)","author":"Black PE","year":"2000"},{"key":"e_1_2_1_73_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSEA.2006.75"},{"issue":"2","key":"e_1_2_1_74_2","first-page":"5","article-title":"Using and improving requirement properties for mutation based test\u2010case generation","volume":"12","author":"Fraser G","year":"2006","journal-title":"22. WI\u2010MAW Rundbrief"},{"key":"e_1_2_1_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-5939-6_5"},{"key":"e_1_2_1_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73770-4_11"},{"key":"e_1_2_1_77_2","unstructured":"OkunV BlackPE YeshaY.Testing with model checker: Insuring fault visibility. Technical Report NIST\u2010IR 6929 National Institute of Standards and Technology 2003."},{"key":"e_1_2_1_78_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"3","volume-title":"Can a Model Checker Generate Tests for Non\u2010deterministic Systems","author":"Boroday S","year":"2007"},{"key":"e_1_2_1_79_2","first-page":"212","volume-title":"Proceedings of the 7th International Conference on Engineering of Complex Computer Systems (ICECCS 2001)","author":"Ammann P","year":"2001"},{"key":"e_1_2_1_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-007-9031-6"},{"key":"e_1_2_1_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/1218776.1218787"},{"key":"e_1_2_1_82_2","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"CAV '00: Proceedings of the 12th International Conference on Computer Aided Verification","author":"Clarke EM","year":"2000"},{"key":"e_1_2_1_83_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"59","volume-title":"Abstractions for Model\u2010Based Testing","author":"Prenninger W","year":"2005"},{"key":"e_1_2_1_84_2","volume-title":"Proceedings of the 18th Digital Avionics Systems Conference","author":"Ammann P","year":"1999"},{"key":"e_1_2_1_85_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSEA.2007.71"},{"key":"e_1_2_1_86_2","series-title":"Lecture Notes in Computer Science","first-page":"42","volume-title":"Third International Workshop on Formal Approaches to Software Testing","author":"Heimdahl MPE","year":"2003"},{"key":"e_1_2_1_87_2","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2004.1281742"},{"key":"e_1_2_1_88_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2005.66"},{"key":"e_1_2_1_89_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2000.873943"},{"key":"e_1_2_1_90_2","unstructured":"OffuttJA VoasJM.Subsumption of condition coverage techniques by mutation testing. Technical Report ISSE\u2010TR\u201096\u201001 1996."},{"key":"e_1_2_1_91_2","unstructured":"BlackPE. Demonstration of generating tests from formal specifications [web page]. URLhttp:\/\/hissa.nist.gov\/black\/AFTG\/[24 October2007]."},{"key":"e_1_2_1_92_2","unstructured":"HamonG de MouraL RushbyJ.Automated test generation with SAL. Technical Report Computer Science Laboratory SRI International 2005."},{"key":"e_1_2_1_93_2","unstructured":"GargantiniA. ATGT: ASM Tests Generation Tool [web page]. URLhttp:\/\/cs.unibg.it\/gargantini\/projects\/atgt\/[25 June2008]."},{"key":"e_1_2_1_94_2","doi-asserted-by":"crossref","unstructured":"BlackPE RanvilleS.Winnowing tests: Getting quality coverage from a model checker without quantity. Digital Avionics Systems 2001. DASC. The 20th Conference vol. 2 2001;9B6\/1\u20139B6\/4.","DOI":"10.1109\/DASC.2001.964253"},{"key":"e_1_2_1_95_2","doi-asserted-by":"publisher","DOI":"10.1145\/152388.152391"},{"key":"e_1_2_1_96_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2004.1342735"},{"key":"e_1_2_1_97_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2007.46"},{"key":"e_1_2_1_98_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71289-3_23"},{"key":"e_1_2_1_99_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2004.1347530"},{"key":"e_1_2_1_100_2","doi-asserted-by":"publisher","DOI":"10.1145\/1291535.1291542"},{"key":"e_1_2_1_101_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1999.792604"},{"key":"e_1_2_1_102_2","first-page":"267","volume-title":"SE'07: Proceedings of the 25th Conference on IASTED International Multi\u2010Conference","author":"Fraser G","year":"2007"},{"key":"e_1_2_1_103_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31848-4_8"},{"key":"e_1_2_1_104_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989799"},{"key":"e_1_2_1_105_2","volume-title":"PADTAD'04, Parallel and Distributed Systems: Testing and Debugging","author":"Barringer H","year":"2004"},{"key":"e_1_2_1_106_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009\u2010003\u20100117\u20106"},{"key":"e_1_2_1_107_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515\u2010005\u20106205\u2010y"},{"key":"e_1_2_1_108_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAICPART.2007.4344120"},{"key":"e_1_2_1_109_2","first-page":"336","volume-title":"COMPSAC '04: Proceedings of the 28th Annual International Computer Software and Applications Conference (COMPSAC'04)","author":"Xu L","year":"2004"},{"key":"e_1_2_1_110_2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"33","volume-title":"Handling Model Changes: Regression Testing and Test\u2010suite Update with Model\u2010checkers","author":"Fraser G","year":"2007"},{"key":"e_1_2_1_111_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24617-6_9"},{"key":"e_1_2_1_112_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_113_2","first-page":"1.B.3\u20131","volume-title":"Proceedings of the 19th Digital Avionics Systems Conference","author":"Black PE","year":"2000"},{"key":"e_1_2_1_114_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_25"},{"key":"e_1_2_1_115_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_5"},{"key":"e_1_2_1_116_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"e_1_2_1_117_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"e_1_2_1_118_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_2_1_119_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48234-2_11"},{"key":"e_1_2_1_120_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873645"},{"key":"e_1_2_1_121_2","first-page":"553","volume-title":"TACAS'03: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Pasareanu CS","year":"2003"},{"key":"e_1_2_1_122_2","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146243"},{"key":"e_1_2_1_123_2","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2002.1224436"},{"key":"e_1_2_1_124_2","first-page":"10182","volume-title":"DATE'04: Proceedings of the Conference on Design, Automation and Test in Europe","author":"Mishra P","year":"2004"},{"key":"e_1_2_1_125_2"},{"key":"e_1_2_1_126_2","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2006.10"},{"key":"e_1_2_1_127_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"SPIN'01: Proceedings of the 8th International SPIN Workshop on Model Checking of Software","author":"Edelkamp S","year":"2001"}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.402","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T22:01:37Z","timestamp":1739311297000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,11]]},"references-count":126,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["10.1002\/stvr.402"],"URL":"https:\/\/doi.org\/10.1002\/stvr.402","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"value":"0960-0833","type":"print"},{"value":"1099-1689","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,11]]}}}