A Formal Interactive Verification Environment for the Plan Execution Interchange Language
The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal ex...
- Autores:
-
Cadavid Rengifo, Hector Fabio
Rocha, Camilo
Muñoz, Cesar
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2012
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1838
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1838
- Palabra clave:
- Comprobación del modelo
Lógica Temporal Lineal
Proposición atómica
Lenguaje síncrono
Estructura Kripke
Model Check
Linear Temporal Logic
Atomic Proposition
Plan Execution
Kripke Structure
- Rights
- closedAccess
- License
- © Springer Nature Switzerland AG 2018
| id |
ESCUELAIG2_619ad9df98dda5acb50b72b2893e02d1 |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1838 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| title |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| spellingShingle |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language Comprobación del modelo Lógica Temporal Lineal Proposición atómica Lenguaje síncrono Estructura Kripke Model Check Linear Temporal Logic Atomic Proposition Plan Execution Kripke Structure |
| title_short |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| title_full |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| title_fullStr |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| title_full_unstemmed |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| title_sort |
A Formal Interactive Verification Environment for the Plan Execution Interchange Language |
| dc.creator.fl_str_mv |
Cadavid Rengifo, Hector Fabio Rocha, Camilo Muñoz, Cesar |
| dc.contributor.author.none.fl_str_mv |
Cadavid Rengifo, Hector Fabio Rocha, Camilo Muñoz, Cesar |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.spa.fl_str_mv |
Comprobación del modelo Lógica Temporal Lineal Proposición atómica Lenguaje síncrono Estructura Kripke |
| topic |
Comprobación del modelo Lógica Temporal Lineal Proposición atómica Lenguaje síncrono Estructura Kripke Model Check Linear Temporal Logic Atomic Proposition Plan Execution Kripke Structure |
| dc.subject.proposal.eng.fl_str_mv |
Model Check Linear Temporal Logic Atomic Proposition Plan Execution Kripke Structure |
| description |
The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model. |
| publishDate |
2012 |
| dc.date.issued.none.fl_str_mv |
2012 |
| dc.date.accessioned.none.fl_str_mv |
2021-11-18T15:39:40Z |
| dc.date.available.none.fl_str_mv |
2021-11-18T15:39:40Z |
| dc.type.spa.fl_str_mv |
Artículo de revista |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_2df8fbb1 |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_3248 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bookPart |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
| format |
http://purl.org/coar/resource_type/c_3248 |
| status_str |
publishedVersion |
| dc.identifier.isbn.none.fl_str_mv |
9783642307294 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1838 |
| identifier_str_mv |
9783642307294 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1838 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.ispartofseries.none.fl_str_mv |
LNCS;Volumen 7321 |
| dc.relation.citationendpage.spa.fl_str_mv |
357 |
| dc.relation.citationstartpage.spa.fl_str_mv |
343 |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.ispartofbook.eng.fl_str_mv |
Lecture Notes in Computer Science |
| dc.relation.references.spa.fl_str_mv |
Balasubramanian, D., Păsăreanu, C., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple Statechart formalisms. In: Dwyer, M.B., Tip, F. (eds.) ISSTA, pp. 45–55. ACM (2011) Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Transactions on Systems, Man, and Cybernetics–Part A: Systems and Humans 41(5), 961–976 (2011) Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006) Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) Dowek, G., Muñoz, C., Păsăreanu, C.: A small-step semantics of PLEXIL. Technical Report 2008-11, National Institute of Aerospace, Hampton, VA (2008) Dowek, G., Muñoz, C., Păsăreanu, C.: A formal analysis framework for PLEXIL. In: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems (September 2007) Dowek, G., Muñoz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. In: Klin, B., Sobocinski, P. (eds.) SOS. EPTCS, vol. 18, pp. 77–91 (2009) Estlin, T., Jónsson, A., Păsăreanu, C., Simmons, R., Tso, K., Verma, V.: Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA (2006) Martí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electronic Notes in Theoretical Computer Science 238(3), 227–247 (2009) Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992) Rocha, C., Muñoz, C., Cadavid, H.: A graphical environment for the semantic validation of a plan execution language. In: IEEE International Conference on Space Mission Challenges for Information Technology, pp. 201–207. IEEE Computer Society, Los Alamitos (2009) Rocha, C., Muñoz, C.: Simulation and Verification of Synchronous Set Relations in Rewriting Logic. In: da Silva Simão, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 60–75. Springer, Heidelberg (2011) Rocha, C., Muñoz, C., Dowek, G.: A formal library of set relations and its application to synchronous languages. Theoretical Computer Science 412(37), 4853–4866 (2011) Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010) Santiago, S., Talcott, C.L., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Electronic Notes in Theoretical Computer Science 258(1), 3–20 (2009) Strauss, P.J.: Executable semantics for PLEXIL: simulating a task-scheduling language in Haskell. Master’s thesis, Oregon State University (2009) Verdejo, A., Martí-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods in System Design 27(1-2), 113–172 (2005) Verma, V., Jónsson, A., Păsăreanu, C., Iatauro, M.: Universal Executive and PLEXIL: Engine and language for robust spacecraft control and operations. In: Proceedings of the American Institute of Aeronautics and Astronautics Space Conference (2006) |
| dc.rights.eng.fl_str_mv |
© Springer Nature Switzerland AG 2018 |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/closedAccess |
| dc.rights.creativecommons.spa.fl_str_mv |
Atribución 4.0 Internacional (CC BY 4.0) |
| rights_invalid_str_mv |
© Springer Nature Switzerland AG 2018 https://creativecommons.org/licenses/by/4.0/ Atribución 4.0 Internacional (CC BY 4.0) http://purl.org/coar/access_right/c_14cb |
| eu_rights_str_mv |
closedAccess |
| dc.format.extent.spa.fl_str_mv |
15 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Springer Nature |
| dc.publisher.place.spa.fl_str_mv |
USA. Switzerland |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1838/7/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language.png https://repositorio.escuelaing.edu.co/bitstream/001/1838/8/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdf.jpg https://repositorio.escuelaing.edu.co/bitstream/001/1838/2/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1838/3/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1838/4/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Languag%20.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1838/6/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdf.txt |
| bitstream.checksum.fl_str_mv |
22153f4f34d3833a0fe40707f659322f 1ca2ce509f3cad8078a6994ce18899f7 ce3159b68d11073dc69f09df67ff8a9d 5a7ca94c2e5326ee169f979d71d0f06e d784fa8b6d98d27699781bd9a7cf19f0 d784fa8b6d98d27699781bd9a7cf19f0 |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1808494268661104640 |
| spelling |
Cadavid Rengifo, Hector Fabioe667daaffd71b986c4bbd7edacec294d600Rocha, Camiloebfd407af468605647a49186059da397600Muñoz, Cesard010620c004c882204e4c6699af11cfa600Informática2021-11-18T15:39:40Z2021-11-18T15:39:40Z20129783642307294https://repositorio.escuelaing.edu.co/handle/001/1838The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.El lenguaje de intercambio de ejecución de planes (PLEXIL) es un lenguaje síncrono de código abierto desarrollado por la NASA para controlar y monitorear sistemas autónomos. Este documento informa sobre el desarrollo del entorno de verificación interactivo formal de PLEXIL (PLEXIL5), una interfaz gráfica para la semántica ejecutable formal de PLEXIL. Entre sus principales características, PLEXIL5 proporciona verificación de modelos de planes con soporte para edición de fórmulas y visualización de contraejemplos, simulación interactiva de planes en diferentes niveles de granularidad e inicialización aleatoria de variables de entorno externo. Las capacidades de verificación formal de PLEXIL5 se ilustran mediante un modelo de interacción humano-automatización.15 páginas.application/pdfengSpringer NatureUSA.SwitzerlandLNCS;Volumen 7321357343N/ALecture Notes in Computer ScienceBalasubramanian, D., Păsăreanu, C., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple Statechart formalisms. In: Dwyer, M.B., Tip, F. (eds.) ISSTA, pp. 45–55. ACM (2011)Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Transactions on Systems, Man, and Cybernetics–Part A: Systems and Humans 41(5), 961–976 (2011)Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)Dowek, G., Muñoz, C., Păsăreanu, C.: A small-step semantics of PLEXIL. Technical Report 2008-11, National Institute of Aerospace, Hampton, VA (2008)Dowek, G., Muñoz, C., Păsăreanu, C.: A formal analysis framework for PLEXIL. In: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems (September 2007)Dowek, G., Muñoz, C., Rocha, C.: Rewriting logic semantics of a plan execution language. In: Klin, B., Sobocinski, P. (eds.) SOS. EPTCS, vol. 18, pp. 77–91 (2009)Estlin, T., Jónsson, A., Păsăreanu, C., Simmons, R., Tso, K., Verma, V.: Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA (2006)Martí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for maude strategies. Electronic Notes in Theoretical Computer Science 238(3), 227–247 (2009)Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)Rocha, C., Muñoz, C., Cadavid, H.: A graphical environment for the semantic validation of a plan execution language. In: IEEE International Conference on Space Mission Challenges for Information Technology, pp. 201–207. IEEE Computer Society, Los Alamitos (2009)Rocha, C., Muñoz, C.: Simulation and Verification of Synchronous Set Relations in Rewriting Logic. In: da Silva Simão, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 60–75. Springer, Heidelberg (2011)Rocha, C., Muñoz, C., Dowek, G.: A formal library of set relations and its application to synchronous languages. Theoretical Computer Science 412(37), 4853–4866 (2011)Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)Santiago, S., Talcott, C.L., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Electronic Notes in Theoretical Computer Science 258(1), 3–20 (2009)Strauss, P.J.: Executable semantics for PLEXIL: simulating a task-scheduling language in Haskell. Master’s thesis, Oregon State University (2009)Verdejo, A., Martí-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods in System Design 27(1-2), 113–172 (2005)Verma, V., Jónsson, A., Păsăreanu, C., Iatauro, M.: Universal Executive and PLEXIL: Engine and language for robust spacecraft control and operations. In: Proceedings of the American Institute of Aeronautics and Astronautics Space Conference (2006)© Springer Nature Switzerland AG 2018https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbA Formal Interactive Verification Environment for the Plan Execution Interchange LanguageArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85Comprobación del modeloLógica Temporal LinealProposición atómicaLenguaje síncronoEstructura KripkeModel CheckLinear Temporal LogicAtomic PropositionPlan ExecutionKripke StructureTHUMBNAILA Formal Interactive Verification Environment for the Plan Execution Interchange Language.pngA Formal Interactive Verification Environment for the Plan Execution Interchange Language.pngimage/png151306https://repositorio.escuelaing.edu.co/bitstream/001/1838/7/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language.png22153f4f34d3833a0fe40707f659322fMD57open accessA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdf.jpgA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdf.jpgGenerated Thumbnailimage/jpeg4996https://repositorio.escuelaing.edu.co/bitstream/001/1838/8/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdf.jpg1ca2ce509f3cad8078a6994ce18899f7MD58metadata only accessORIGINALA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdfA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdfapplication/pdf114783https://repositorio.escuelaing.edu.co/bitstream/001/1838/2/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdfce3159b68d11073dc69f09df67ff8a9dMD52metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1838/3/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD53open accessTEXTA Formal Interactive Verification Environment for the Plan Execution Interchange Languag .pdf.txtA Formal Interactive Verification Environment for the Plan Execution Interchange Languag .pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1838/4/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Languag%20.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD54open accessA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdf.txtA Formal Interactive Verification Environment for the Plan Execution Interchange Language .pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1838/6/A%20Formal%20Interactive%20Verification%20Environment%20for%20the%20Plan%20Execution%20Interchange%20Language%20.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD56open access001/1838oai:repositorio.escuelaing.edu.co:001/18382022-12-13 03:01:10.8metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |