Synchronous set relations in rewriting logic
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure, which is written in the Maude system, enabl...
- Autores:
-
Muñoz, César
Rocha Niño, Hernán Camilo
- Tipo de recurso:
- Article of journal
- Fecha de publicación:
- 2014
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1864
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1864
- Palabra clave:
- Relaciones de conjuntos sincrónicos
semántica síncrona
Reescritura de lógica
Simulación formal y verificación
Maude
Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL
- Rights
- openAccess
- License
- © 2013 Elsevier B.V. Published by Elsevier B.V. All rights reserved.
id |
ESCUELAIG2_bf60fa8685813185da5500e138b74007 |
---|---|
oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1864 |
network_acronym_str |
ESCUELAIG2 |
network_name_str |
Repositorio Institucional ECI |
repository_id_str |
|
dc.title.eng.fl_str_mv |
Synchronous set relations in rewriting logic |
title |
Synchronous set relations in rewriting logic |
spellingShingle |
Synchronous set relations in rewriting logic Relaciones de conjuntos sincrónicos semántica síncrona Reescritura de lógica Simulación formal y verificación Maude Synchronous set relations Synchronous semantics Rewriting logic Formal simulation and verification PLEXIL |
title_short |
Synchronous set relations in rewriting logic |
title_full |
Synchronous set relations in rewriting logic |
title_fullStr |
Synchronous set relations in rewriting logic |
title_full_unstemmed |
Synchronous set relations in rewriting logic |
title_sort |
Synchronous set relations in rewriting logic |
dc.creator.fl_str_mv |
Muñoz, César Rocha Niño, Hernán Camilo |
dc.contributor.author.none.fl_str_mv |
Muñoz, César Rocha Niño, Hernán Camilo |
dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
dc.subject.armarc.spa.fl_str_mv |
Relaciones de conjuntos sincrónicos semántica síncrona Reescritura de lógica Simulación formal y verificación |
topic |
Relaciones de conjuntos sincrónicos semántica síncrona Reescritura de lógica Simulación formal y verificación Maude Synchronous set relations Synchronous semantics Rewriting logic Formal simulation and verification PLEXIL |
dc.subject.armarc.eng.fl_str_mv |
Maude |
dc.subject.proposal.eng.fl_str_mv |
Synchronous set relations Synchronous semantics Rewriting logic Formal simulation and verification PLEXIL |
description |
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations. |
publishDate |
2014 |
dc.date.issued.none.fl_str_mv |
2014 |
dc.date.accessioned.none.fl_str_mv |
2021-11-27T16:38:47Z |
dc.date.available.none.fl_str_mv |
2021-11-27T16:38:47Z |
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_6501 |
dc.type.content.spa.fl_str_mv |
Text |
dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/article |
dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
format |
http://purl.org/coar/resource_type/c_6501 |
status_str |
publishedVersion |
dc.identifier.issn.none.fl_str_mv |
01676423 |
dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1864 |
identifier_str_mv |
01676423 |
url |
https://repositorio.escuelaing.edu.co/handle/001/1864 |
dc.language.iso.spa.fl_str_mv |
eng |
language |
eng |
dc.relation.citationendpage.spa.fl_str_mv |
228 |
dc.relation.citationstartpage.spa.fl_str_mv |
211 |
dc.relation.citationvolume.spa.fl_str_mv |
92 |
dc.relation.indexed.spa.fl_str_mv |
N/A |
dc.relation.ispartofjournal.eng.fl_str_mv |
Science of Computer Programming |
dc.relation.references.spa.fl_str_mv |
1] M. AlTurki, J. Meseguer, Reduction semantics and formal analysis of Orc programs, in: Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, WWV 2007, Electron. Notes Theor. Comput. Sci. 200 (3) (2008) 25–41 R. Bruni, J. Meseguer, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci. 360 (1–3) (2006) 386–414. C. Chira, T.F. Serbanuta, G. Stefanescu, P systems with control nuclei: The concept, J. Log. Algebr. Program. 79 (6) (2010) 326–333, Membrane computing and programming M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C.L. Talcott (Eds.), All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350, Springer, 2007. M. Clavel, J. Meseguer, M. Palomino, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theor. Comput. Sci. 373 (1–2) (2007) 70–91. G. Dowek, C. Muñoz, C. Pas˘ areanu, A small-step semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008. G. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, Electron. Proc. Theor. Comput. Sci. 18 (2010) 77–91. T. Estlin, A. Jónsson, C. Pas˘ areanu, R. Simmons, K. Tso, V. Verna, Plan Execution Interchange Language (PLEXIL), Technical Memorandum ˘ TM-2006-213483, NASA, 2006. [9] D. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, in: Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2008, Electron. Notes Theor. Comput. Sci. 237 (2009) 107–125. N. Martí-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, Electron. Notes Theor. Comput. Sci. 238 (3) (2009) 227–247. [11] J. Meseguer, Membership algebra as a logical framework for equational specification, in: F. Parisi-Presicce (Ed.), WADT, in: Lect. Notes Comput. Sci., vol. 1376, Springer, 1997, pp. 18–61. J. Meseguer, P. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, in: J. Dong, H. Zhu (Eds.), Formal Methods and Software Engineering, in: Lect. Notes Comput. Sci., vol. 6447, Springer, Berlin / Heidelberg, 2010, pp. 303–320. C. Rocha, Symbolic reachability analysis for rewrite theories, PhD thesis, University of Illinois at Urbana-Champaign, December 2012, https://www. ideals.illinois.edu/handle/2142/42200. C. Rocha, H. Cadavid, C. Muñoz, R. Siminiceanu, A formal interactive verification environment for the plan execution interchange language, in: D. Latella, H. Treharne (Eds.), Proceedings of 9th International Conference on Integrated Formal Methods, iFM 2012, Pisa, Italy, in: Lect. Notes Comput. Sci., vol. 7321, June 2012, pp. 343–357. C. Rocha, J. Meseguer, Proving safety properties of rewrite theories, in: A. Corradini, B. Klin, C. Cîrstea (Eds.), CALCO, in: Lect. Notes Comput. Sci., vol. 6859, Springer, 2011, pp. 314–328. C. Rocha, C. Muñoz, G. Dowek, A formal library of set relations and its application to synchronous languages, Theor. Comput. Sci. 412 (37) (2011) 4853–4866. T. Serbanuta, A rewriting approach to concurrent programming language design and semantics, PhD thesis, University of Illinois at Urbana-Champaign, December 2010, https://www.ideals.illinois.edu/handle/2142/18252. T. Serbanuta, G. Stefanescu, G. Rosu, Defining and executing P systems with structured data in K, in: D. Corne, P. Frisco, G. Paun, G. Rozenberg, A. Salomaa (Eds.), Membrane Computing, in: Lect. Notes Comput. Sci., vol. 5391, Springer, Berlin/Heidelberg, 2009, pp. 374–393 Universities Space Research Association, The Plan Execution Interchange Language, http://plexil.sourceforge.net, June 2006. P. Viry, Equational rules for rewriting logic, Theor. Comput. Sci. 285 (2) (2002) 487–517 |
dc.rights.eng.fl_str_mv |
© 2013 Elsevier B.V. Published by Elsevier B.V. All rights reserved. |
dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_abf2 |
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/openAccess |
dc.rights.creativecommons.spa.fl_str_mv |
Atribución 4.0 Internacional (CC BY 4.0) |
rights_invalid_str_mv |
© 2013 Elsevier B.V. Published by Elsevier B.V. All rights reserved. https://creativecommons.org/licenses/by/4.0/ Atribución 4.0 Internacional (CC BY 4.0) http://purl.org/coar/access_right/c_abf2 |
eu_rights_str_mv |
openAccess |
dc.format.extent.spa.fl_str_mv |
18 páginas. |
dc.format.mimetype.spa.fl_str_mv |
application/pdf |
dc.publisher.spa.fl_str_mv |
Elsevier |
dc.source.spa.fl_str_mv |
https://www.sciencedirect.com/science/article/pii/S0167642313001652 |
institution |
Escuela Colombiana de Ingeniería Julio Garavito |
bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1864/1/Synchronous%20set%20relations%20in%20rewriting%20logic.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1864/2/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1864/3/Synchronous%20set%20relations%20in%20rewriting%20logic.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1864/4/Synchronous%20set%20relations%20in%20rewriting%20logic.pdf.jpg |
bitstream.checksum.fl_str_mv |
cba722b1338b046d1b858af56d3444a3 5a7ca94c2e5326ee169f979d71d0f06e ac4b9b59c9f592750638b1c6614c87ac bd56c46918a9a0dd96232e2bfbd0409c |
bitstream.checksumAlgorithm.fl_str_mv |
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_ |
1814355639628988416 |
spelling |
Muñoz, César70953c4ce36fbd95e2df915d4688e3b1600Rocha Niño, Hernán Camilo731e751c2ace8f3033b68d89ea2d3665600Informática2021-11-27T16:38:47Z2021-11-27T16:38:47Z201401676423https://repositorio.escuelaing.edu.co/handle/001/1864This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.Este artículo presenta una base matemática y una infraestructura lógica de reescritura para la ejecución y verificación de propiedades de relaciones de conjuntos sincrónicos. El fundamento matemático se da en el lenguaje de las relaciones abstractas de conjuntos. La infraestructura, que está escrita en el sistema Maude, permite la ejecución sincrónica de una relación establecida proporcionada por el usuario. Mediante el uso de la infraestructura, las técnicas de verificación de algoritmos, como el análisis de accesibilidad y la verificación de modelos, ya disponibles en Maude para la reescritura asincrónica tradicional, están disponibles automáticamente para la reescritura sincrónica de conjuntos. De esta manera, los lenguajes y sistemas sincrónicos basados en conjuntos, como los construidos a partir de agentes, componentes u objetos, pueden especificarse y simularse de forma natural, y también son susceptibles de verificación formal en el sistema Maude. El uso de la infraestructura y algunas de sus capacidades de verificación basadas en Maude se ilustran con una semántica operativa ejecutable del lenguaje de intercambio de ejecución del plan (PLEXIL), un lenguaje síncrono desarrollado por la NASA para respaldar las operaciones de naves espaciales autónomas.18 páginas.application/pdfengElsevier© 2013 Elsevier B.V. Published by Elsevier B.V. All rights reserved.https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/openAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_abf2https://www.sciencedirect.com/science/article/pii/S0167642313001652Synchronous set relations in rewriting logicArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_6501http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/articlehttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a8522821192N/AScience of Computer Programming1] M. AlTurki, J. Meseguer, Reduction semantics and formal analysis of Orc programs, in: Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, WWV 2007, Electron. Notes Theor. Comput. Sci. 200 (3) (2008) 25–41R. Bruni, J. Meseguer, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci. 360 (1–3) (2006) 386–414.C. Chira, T.F. Serbanuta, G. Stefanescu, P systems with control nuclei: The concept, J. Log. Algebr. Program. 79 (6) (2010) 326–333, Membrane computing and programmingM. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C.L. Talcott (Eds.), All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350, Springer, 2007.M. Clavel, J. Meseguer, M. Palomino, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theor. Comput. Sci. 373 (1–2) (2007) 70–91.G. Dowek, C. Muñoz, C. Pas˘ areanu, A small-step semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.G. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, Electron. Proc. Theor. Comput. Sci. 18 (2010) 77–91.T. Estlin, A. Jónsson, C. Pas˘ areanu, R. Simmons, K. Tso, V. Verna, Plan Execution Interchange Language (PLEXIL), Technical Memorandum ˘ TM-2006-213483, NASA, 2006.[9] D. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, in: Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2008, Electron. Notes Theor. Comput. Sci. 237 (2009) 107–125.N. Martí-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, Electron. Notes Theor. Comput. Sci. 238 (3) (2009) 227–247.[11] J. Meseguer, Membership algebra as a logical framework for equational specification, in: F. Parisi-Presicce (Ed.), WADT, in: Lect. Notes Comput. Sci., vol. 1376, Springer, 1997, pp. 18–61.J. Meseguer, P. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, in: J. Dong, H. Zhu (Eds.), Formal Methods and Software Engineering, in: Lect. Notes Comput. Sci., vol. 6447, Springer, Berlin / Heidelberg, 2010, pp. 303–320.C. Rocha, Symbolic reachability analysis for rewrite theories, PhD thesis, University of Illinois at Urbana-Champaign, December 2012, https://www. ideals.illinois.edu/handle/2142/42200.C. Rocha, H. Cadavid, C. Muñoz, R. Siminiceanu, A formal interactive verification environment for the plan execution interchange language, in: D. Latella, H. Treharne (Eds.), Proceedings of 9th International Conference on Integrated Formal Methods, iFM 2012, Pisa, Italy, in: Lect. Notes Comput. Sci., vol. 7321, June 2012, pp. 343–357.C. Rocha, J. Meseguer, Proving safety properties of rewrite theories, in: A. Corradini, B. Klin, C. Cîrstea (Eds.), CALCO, in: Lect. Notes Comput. Sci., vol. 6859, Springer, 2011, pp. 314–328.C. Rocha, C. Muñoz, G. Dowek, A formal library of set relations and its application to synchronous languages, Theor. Comput. Sci. 412 (37) (2011) 4853–4866.T. Serbanuta, A rewriting approach to concurrent programming language design and semantics, PhD thesis, University of Illinois at Urbana-Champaign, December 2010, https://www.ideals.illinois.edu/handle/2142/18252.T. Serbanuta, G. Stefanescu, G. Rosu, Defining and executing P systems with structured data in K, in: D. Corne, P. Frisco, G. Paun, G. Rozenberg, A. Salomaa (Eds.), Membrane Computing, in: Lect. Notes Comput. Sci., vol. 5391, Springer, Berlin/Heidelberg, 2009, pp. 374–393Universities Space Research Association, The Plan Execution Interchange Language, http://plexil.sourceforge.net, June 2006.P. Viry, Equational rules for rewriting logic, Theor. Comput. Sci. 285 (2) (2002) 487–517Relaciones de conjuntos sincrónicossemántica síncronaReescritura de lógicaSimulación formal y verificaciónMaudeSynchronous set relationsSynchronous semanticsRewriting logicFormal simulation and verificationPLEXILORIGINALSynchronous set relations in rewriting logic.pdfSynchronous set relations in rewriting logic.pdfArtículo principal.application/pdf423514https://repositorio.escuelaing.edu.co/bitstream/001/1864/1/Synchronous%20set%20relations%20in%20rewriting%20logic.pdfcba722b1338b046d1b858af56d3444a3MD51metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1864/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTSynchronous set relations in rewriting logic.pdf.txtSynchronous set relations in rewriting logic.pdf.txtExtracted texttext/plain78811https://repositorio.escuelaing.edu.co/bitstream/001/1864/3/Synchronous%20set%20relations%20in%20rewriting%20logic.pdf.txtac4b9b59c9f592750638b1c6614c87acMD53open accessTHUMBNAILSynchronous set relations in rewriting logic.pdf.jpgSynchronous set relations in rewriting logic.pdf.jpgGenerated Thumbnailimage/jpeg14903https://repositorio.escuelaing.edu.co/bitstream/001/1864/4/Synchronous%20set%20relations%20in%20rewriting%20logic.pdf.jpgbd56c46918a9a0dd96232e2bfbd0409cMD54open access001/1864oai:repositorio.escuelaing.edu.co:001/18642022-07-18 08:55:22.14metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |