From e33be76d23718889bbc811c70d9e28526fb9a347 Mon Sep 17 00:00:00 2001 From: couchot Date: Thu, 28 Nov 2013 21:43:34 +0100 Subject: [PATCH] initial --- bib/abbrev.bib | 20 + bib/biblioand.bib | 521 ++++++++++++++++++++++ modes/promela-mode.el | 985 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 1526 insertions(+) create mode 100755 bib/abbrev.bib create mode 100644 bib/biblioand.bib create mode 100644 modes/promela-mode.el diff --git a/bib/abbrev.bib b/bib/abbrev.bib new file mode 100755 index 0000000..f2de8e2 --- /dev/null +++ b/bib/abbrev.bib @@ -0,0 +1,20 @@ + + +@String{elsevier={Elsevier Science Publishers B. V.}} +@String{springer={Springer}} + + + +@String{NC = {Neural Computation}} +@String{TNN= {IEEE Transactions on Neural Networks}} +@String{STTT= {International Journal on Software Tools for Technology Transfer}} +@string{JACM={Journal of ACM}} +@String{JCAM={Journal of Computational and Applied Mathematics}} +@String{lncs={Lecture Notes in Computer Science}} +@String{tcs={Theoretical Computer Science}} +@String{jtb={Journal of Theoretical Biology}} +@string{prenticeHall={Prentice-Hall, Inc.}} +@string{discreteapplMath={Discrete Applied Mathematics}} +@string{advapplMath={Advances in Applied Mathematics}} +@string{ijma= {International Journal of Mathematical Algorithms}} +@string{cs= {Cognitive Science}} diff --git a/bib/biblioand.bib b/bib/biblioand.bib new file mode 100644 index 0000000..4da6eec --- /dev/null +++ b/bib/biblioand.bib @@ -0,0 +1,521 @@ +c% This file was created with JabRef 2.3.1. +% Encoding: ANSI_X3.4-1968 + +@INPROCEEDINGS{nusmv02, + author = {Alessandro Cimatti and Edmund M. Clarke and Enrico Giunchiglia and + Fausto Giunchiglia and Marco Pistore and Marco Roveri and Roberto + Sebastiani and Armando Tacchella}, + title = {NuSMV 2: An OpenSource Tool for Symbolic Model Checking}, + booktitle = {CAV}, + year = {2002}, + pages = {359-364}, + crossref = {DBLP:conf/cav/2002} +} + +@INPROCEEDINGS{CGK05, + author = {Jean-Fran\c{c}ois Couchot and Alain Giorgetti and Nikolai Kosmatov}, + title = {A uniform deductive approach for parameterized protocol safety}, + booktitle = {ASE}, + year = {2005}, + pages = {364-367}, + bibsource = {DBLP, http://dblp.uni-trier.de}, + crossref = {DBLP:conf/kbse/2005}, + ee = {http://doi.acm.org/10.1145/1101908.1101971} +} + +@INPROCEEDINGS{abcvs05, + author = {Abbas, A. and Bahi, J. M. and Contassot-Vivier, S. and Salomon, M.}, + title = {Mixing Synchronism / Asynchronism in Discrete-State Discrete-Time + Dynamic Networks}, + booktitle = {4th Int. Conf. on Engineering Applications and Computational Algorithms, + DCDIS'2005}, + year = {2005}, + pages = {524--529}, + address = {Guelph, Canada}, + month = jul, + note = {ISSN 1492-8760} +} + +@ARTICLE{Bah00, + author = {Bahi, J. M.}, + title = {Boolean totally asynchronous iterations}, + journal = ijma, + year = {2000}, + volume = {1}, + pages = {331--346} +} + +@ARTICLE{BCV06, + author = {Bahi, J. M. and Contassot-Vivier, S.}, + title = {Basins of attraction in fully asynchronous discrete-time discrete-state + dynamic networks}, + journal = TNN, + year = {2006}, + volume = {17}, + pages = {397-408}, + number = {2} +} + +@ARTICLE{bcv02, + author = {Bahi, J. M. and Contassot-Vivier, S.}, + title = {Stability of fully asynchronous discrete-time discrete-state dynamic + networks}, + journal = TNN, + year = {2002}, + volume = {13}, + pages = {1353--1363}, + number = {6} +} + +@techreport{BCVC10:ir, + author = {Bahi, J. M. and Contassot-Vivier, S. and Couchot, J.-F.}, + title = {Convergence Results of Combining Synchronism and Asynchronism for + Discrete-State Discrete-Time Dynamic Network}, + year = {2010}, + institution = {LIFC - Laboratoire d’{I}nformatique de + l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}}, + type = {Research Report}, + number = {RR2010-02}, + pdf = {/publis/papers/pub/2010/RR2010-02.pdf}, + month = may + } + +@techreport{Cou10:ir, + author = {Couchot, J.-F.}, + title = {Formal {C}onvergence {P}roof for {D}iscrete +{D}ynamical {S}ystems}, + year = {2010}, + institution = {LIFC - Laboratoire d’{I}nformatique de + l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}}, + type = {Research Report}, + number = {RR2010-03}, + pdf = {/publis/papers/pub/2010/RR2010-03.pdf}, + month = may, + year = 2010 + } + + + +@ARTICLE{BM00, + author = {Bahi, J. M. and Michel, C.}, + title = {Convergence of discrete asynchronous iterations}, + journal = {International Journal Computer Mathematics}, + year = {2000}, + volume = {74}, + pages = {113--125} +} + +@ARTICLE{BM99, + author = {Bahi, J. M. and Michel, C.}, + title = {Simulations of asynchronous evolution of discrete systems}, + journal = {Simulation Practice and Theory}, + year = {1999}, + volume = {7}, + pages = {309--324} +} + + +@ARTICLE{Bau78, + author = {G\'{e}rard M. Baudet}, + title = {Asynchronous Iterative Methods for Multiprocessors}, + journal = JACM, + year = {1978}, + volume = {25}, + pages = {226--244}, + number = {2}, + doi = {http://doi.acm.org/10.1145/322063.322067}, + issn = {0004-5411}, + publisher = {ACM} +} + +@BOOK{BT89, + title = {Parallel and distributed computation: numerical methods}, + publisher = prenticeHall, + year = {1989}, + author = {Dimitri P. Bertsekas and John N. Tsitsiklis}, + isbn = {0-13-648700-9} +} + +@ARTICLE{blast07, + author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, + title = {The software model checker Blast}, + journal = STTT, + year = {2007}, + volume = {9}, + pages = {505-525}, + number = {5-6} +} + +@INPROCEEDINGS{LeCun85, + author = {Y Le~Cun}, + title = {A learning scheme for threshold networks}, + booktitle = {Cognitiva'95}, + year = {1985}, + pages = {599--604}, + address = {Paris, France} +} + +@ARTICLE{Elm90, + author = {Jeffrey L. Elman}, + title = {Finding Structure in Time}, + journal = {Cognitive Science}, + year = {1990}, + volume = {14}, + pages = {179--211} +} + +@ARTICLE{FS00, + author = {Andreas Frommer and Daniel B. Szyld}, + title = {On asynchronous iterations}, + journal = JCAM, + year = {2000}, + volume = {123}, + pages = {201--216}, + number = {1-2}, + doi = {http://dx.doi.org/10.1016/S0377-0427(00)00409-X}, + issn = {0377-0427}, + publisher = elsevier +} + +@ARTICLE{GS08, + author = {Goles Ch., E. and Salinas,L.}, + title = {Comparison between parallel and serial dynamics of Boolean networks}, + journal = tcs, + year = {2008}, + volume = {396}, + pages = {247--253}, + number = {1-3} +} + +@BOOK{Hol03, + title = {The SPIN Model Checker: Primer and Reference Manual}, + publisher = {Addison-Wesley, Pearson Education}, + year = {2003}, + author = {Gerard J. Holzmann} +} + +@ARTICLE{SH99, + author = {Shih M.-H. and Ho, J.-L.}, + title = {Solution of the Boolean Markus-Yamabe Problem}, + journal = advapplMath, + year = {1999}, + volume = {22}, + pages = {60 - 102}, + number = {1} +} + +@ARTICLE{Ric08, + author = {Adrien Richard}, + title = {An extension of a combinatorial fixed point theorem of Shih and Dong + }, + journal = advapplMath, + year = {2008}, + volume = {41}, + pages = {620--627}, + number = {4}, + publisher = elsevier +} + +@ARTICLE{RC07, + author = {Adrien Richard and Jean-Paul Comet}, + title = {Necessary conditions for multistationarity in discrete dynamical + systems}, + journal = discreteapplMath, + year = {2007}, + volume = {155}, + pages = {2403--2413}, + number = {18}, + issn = {0166-218X}, + publisher = elsevier +} + +@BOOK{Rob95, + title = {Les syst\`emes dynamiques discrets}, + publisher = springer, + year = {1995}, + author = {F. Robert}, + volume = {19}, + series = {Math\'ematiques et Applications} +} + +@ARTICLE{SD05, + author = {Shih, M.-H. and Dong J.-L.}, + title = {A combinatorial analogue of the Jacobian problem in automata networks}, + journal = advapplMath, + year = {2005}, + volume = {34}, + pages = {30 - 46}, + number = {1}, + issn = {0196-8858} +} + +@ARTICLE{Tho73, + author = {Thomas, R.}, + title = {Boolean Formalization of Genetic Control Circuits}, + journal = jtb, + year = {1973}, + volume = {42}, + pages = {563--585} +} + +@ARTICLE{WJBG98, + author = {Xin Wang and Arun K. Jagota and Fernanda Botelho and Max H. Garzon}, + title = {Absence of Cycles in Symmetric Neural Networks}, + journal = NC, + year = {1998}, + volume = {10}, + pages = {1235-1249}, + number = {5}, + file = {:/home/couchot/rech/Ref/WJBG98.pdf:PDF} +} + +@PROCEEDINGS{DBLP:conf/cav/2002, + title = {Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, + Denmark, July 27-31, 2002, Proceedings}, + year = {2002}, + editor = {Ed Brinksma and Kim Guldstrand Larsen}, + volume = {2404}, + series = lncs, + publisher = springer, + booktitle = {CAV} +} + +@PROCEEDINGS{DBLP:conf/kbse/2005, + title = {20th IEEE/ACM International Conference on Automated Software Engineering + (ASE 2005), November 7-11, 2005, Long Beach, CA, USA}, + year = {2005}, + editor = {David F. Redmiles and Thomas Ellman and Andrea Zisman}, + publisher = {ACM}, + bibsource = {DBLP, http://dblp.uni-trier.de}, + booktitle = {ASE} +} + +@book{Mor08, + author = {Ben-Ari, Mordechai}, + year = {2008}, + title = {Principles of the Spin Model Checker}, + isbn = {1846287693, 9781846287695}}, + publisher = springer, + } + + +@INPROCEEDINGS{Wei97, + author = {Weise,Carsten}, + title = {An incremental formal semantics for {PROMELA}}, + booktitle = {SPIN97, the Third SPIN Workshop}, + year = {1997}, + pages = {} +} + +@PHDTHESIS{Couchot-PhD06, + AUTHOR = {Couchot, Jean-Fran\c{c}ois}, + TITLE = {V\'erification d'invariant de syst\`emes param\'etr\'es par + superposition}, + MONTH = {avril}, + SCHOOL = {LIFC, Universit\'e de Franche-Comt\'e}, + TYPE = {Th\`ese de {D}octorat}, + YEAR = {2006} +} + +@Article{dJGH04, + author = {de Jong, H. and Gouz\'e, J.-L. and Hernandez, C. and + Page, M. and Tewfik, S. and Geiselmann, J.}, + title = {Qualitative simulation of genetic regulatory networks + using piecewise-linear models}, + journal = {Bull. Math. Biol.}, + year = {2004}, + OPTkey = {}, + volume = {66}, + number = {2}, + pages = {301--340}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + +@Article{BCRG04, + author = {Bernot, G. and Comet, J.-P. and Richard, A. and Guespin, J.}, + title = {A Fruitful Application of Formal Methods to Biological + Regulatory Networks: Extending {T}homas' Asynchronous + Logical Approach with Temporal Logic}, + journal = {J. Theor. Biol.}, + year = {2004}, + volume = {229}, + number = {3}, + pages = {339--347}, + EQUIPE = {bioinfo}, + KIND = {intrevue} +} + +@Article{GN06, + author = {Gonzales, A.G. and Naldi, A. and S\'anchez, L. and Thieffry, D. and Chaouiya, C.}, + title = {{GINsim}: a software suite for the qualitative modelling, simulation and analysis of regulatory networks}, + journal = {Biosystems}, + year = {2006}, + OPTkey = {}, + volume = {84}, + number = {2}, + pages = {91--100}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + +@Article{dJGH03, + author = {De Jong, H. and Geiselmann, J. and Hernandez, C. and + Page, M.}, + title = {Genetic Network Analyzer: qualitative simulation + of genetic regulatory networks.}, + journal = {Bioinformatics}, + year = {2003}, + volume = {19}, + number = {3}, + pages = {336-44.} +} + +@Article{KCRB09, + author = {Khalis, Z. and Comet, J.-P. and Richard, A. and Bernot, G.}, + title = {The SMBioNet Method for Discovering Models of Gene Regulatory Networks}, + journal = {Genes, Genomes and Genomics}, + year = {2009}, + OPTkey = {}, + volume = {3}, + number = {1}, + OPTpages = {15-22}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + +@article{ARBCR08, + author = {Ahmad, Jamil and Roux, Olivier and Bernot, Gilles and Comet, Jean-Paul and Richard, Adrien}, + title = {Analysing formal models of genetic regulatory networks with delays}, + journal = {Int. J. Bioinformatics Res. Appl.}, + volume = {4}, + number = {3}, + year = {2008}, + issn = {1744-5485}, + pages = {240--262}, + doi = {http://dx.doi.org/10.1504/IJBRA.2008.019573}, + publisher = {Inderscience Publishers}, + address = {Inderscience Publishers, Geneva, SWITZERLAND}, + } +@TechReport{R09-c, + author = {Richard, A.}, + title = {Local negative circuits and fixed points in Boolean networks}, + institution = {preprint arXiv number 0910.0750}, + year = {2009}, + OPTkey = {}, + OPTtype = {}, + OPTnumber = {}, + OPTaddress = {}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + + +@ARTICLE{RRT08, + author = {Remy, R. and Ruet, P. and Thieffry, D.}, + title = {Graphic requirement for multistability and attractive cycles in a + Boolean dynamical framework}, + journal = {Advances in Applied Mathematics}, + year = {2008}, + volume = {41}, + pages = {335-350}, + number = {3}, + owner = {couchot}, + timestamp = {2009.02.05} +} + +@inproceedings{DBLP:conf/icann/BahiCMMS06, + author = {Jacques M. Bahi and + Sylvain Contassot-Vivier and + Libor Makovicka and + {\'E}ric Martin and + Marc Sauget}, + title = {Neural Network Based Algorithm for Radiation Dose Evaluation + in Heterogeneous Environments}, + booktitle = {ICANN (2)}, + year = {2006}, + pages = {777-787}, + ee = {http://dx.doi.org/10.1007/11840930_81}, + crossref = {DBLP:conf/icann/2006-2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/icann/2006-2, + editor = {Stefanos D. Kollias and + Andreas Stafylopatis and + Wlodzislaw Duch and + Erkki Oja}, + title = {Artificial Neural Networks - ICANN 2006, 16th International + Conference, Athens, Greece, September 10-14, 2006. Proceedings, + Part II}, + booktitle = {ICANN (2)}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {4132}, + year = {2006}, + isbn = {3-540-38871-0}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + + + +@Book{Drey08, + author = {Dreyfus, Gérard and Martinez, Jean-Marc and Samuelides, Manuel and Gordon, Mirta B. and Badran, Fouad and Thiria, Sylvie }, + ALTeditor = {}, + title = {Apprentissage statistique, Réseaux de neurones - Cartes topologiques - Machines à vecteurs supports}, + publisher = {Eyrolles}, + year = {2008}, + OPTkey = {}, + OPTvolume = {}, + OPTnumber = {}, + OPTseries = {}, + OPTaddress = {}, + OPTedition = {}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + + + +@CONFERENCE{wang2009, + author = {Q Wang and C Guyeux and J M. Bahi}, + title = {A novel pseudo-random generator based on discrete chaotic +iterations for cryptographic applications}, + booktitle = {First International Conference on Evolving Internet}, + year = {2009}, + owner = {qianxue}, + timestamp = {2009.10.29} +} + + +@BOOK{Dev89, + title = {An Introduction to Chaotic Dynamical Systems}, + publisher = {Redwood City: Addison-Wesley}, + year = {1989}, + author = {R. L. Devaney}, + edition = {2nd}, + owner = {guyeux}, + timestamp = {27/01/2008} +} + + + + + +@ARTICLE{guyeux09-b, + author = {Guyeux, Christophe and Bahi, J. M.}, + title = {Hash functions using chaotic iterations}, + journal = {Journal of Algorithms \& Computational Technology}, + year = {2009}, + note = {To appear}, + owner = {guyeux}, + timestamp = {2009.07.12} +} + + diff --git a/modes/promela-mode.el b/modes/promela-mode.el new file mode 100644 index 0000000..10cac3f --- /dev/null +++ b/modes/promela-mode.el @@ -0,0 +1,985 @@ +;; promela-mode.el --- major mode for editing PROMELA program files +;; $Revision: 1.11 $ $Date: 2001/07/09 18:36:45 $ $Author: engstrom $ + +;; Author: Eric Engstrom +;; Maintainer: Eric Engstrom +;; Keywords: spin, promela, tools + +;; Copyright (C) 1998-2003 Eric Engstrom / Honeywell Laboratories + +;; ... Possibly insert GPL here someday ... + +;;; Commentary: + +;; This file contains code for a GNU Emacs major mode for editing +;; PROMELA (SPIN) program files. + +;; Type "C-h m" in Emacs (while in a buffer in promela-mode) for +;; information on how to configure indentation and fontification, +;; or look at the configuration variables below. + +;; To use, place promela-mode.el in a directory in your load-path. +;; Then, put the following lines into your .emacs and promela-mode +;; will be automatically loaded when editing a PROMELA program. + +;; (autoload 'promela-mode "promela-mode" "PROMELA mode" nil t) +;; (setq auto-mode-alist +;; (append +;; (list (cons "\\.promela$" 'promela-mode) +;; (cons "\\.spin$" 'promela-mode) +;; (cons "\\.pml$" 'promela-mode) +;; ;; (cons "\\.other-extensions$" 'promela-mode) +;; ) +;; auto-mode-alist)) + +;; If you wish for promela-mode to be used for files with other +;; extensions you add your own patterned after the code above. + +;; Note that promela-mode adhears to the font-lock "standards" and +;; defines several "levels" of fontification or colorization. The +;; default is fairly gaudy, so I can imagine that some folks would +;; like a bit less. FMI: see `font-lock-maximum-decoration' + +;; This mode is known to work under the following versions of emacs: +;; - XEmacs: 19.16, 20.x, 21.x +;; - FSF/GNU Emacs: 19.34 +;; - NTEmacs (FSF): 20.[67] +;; That is not to say there are no bugs specific to one of those versions :-) + +;; Please send any comments, bugs, patches or other requests to +;; Eric Engstrom at engstrom@htc.honeywell.com + +;; To-Do: +;; - compile/syntax-check/verify? (suggested by R.Goldman) +;; - indentation - splitting lines at logical operators (M. Rangarajan) +;; [ This might "devolve" to indentation after "->" or ";" +;; being as is, but anything else indent even more? ] +;; :: SomeReallyLongArrayRef[this].typedefField != SomeReallyLongConstant -> /* some-comment */ +;; [ Suggestion would be to break the first line after the !=, therefore: ] +;; :: SomeReallyLongArrayRef[this].typedefField +;; != SomeReallyLongConstant -> /* some-comment */ +;; [ at this point I'm not so sure about this change... EE: 2001/05/19 ] + +;;; ------------------------------------------------------------------------- +;;; Code: + +;; NOTE: same as CVS revision: +(defconst promela-mode-version "$Revision: 1.11 $" + "Promela-mode version number.") + +;; ------------------------------------------------------------------------- +;; The following constant values can be modified by the user in a .emacs file + +(defconst promela-block-indent 2 + "*Controls indentation of lines within a block (`{') construct") + +(defconst promela-selection-indent 2 + "*Controls indentation of options within a selection (`if') +or iteration (`do') construct") + +(defconst promela-selection-option-indent 3 + "*Controls indentation of lines after options within selection or +iteration construct (`::')") + +(defconst promela-comment-col 32 + "*Defines the desired comment column for comments to the right of text.") + +(defconst promela-tab-always-indent t + "*Non-nil means TAB in Promela mode should always reindent the current line, +regardless of where in the line point is when the TAB command is used.") + +(defconst promela-auto-match-delimiter t + "*Non-nil means typing an open-delimiter (i.e. parentheses, brace, quote, etc) +should also insert the matching closing delmiter character.") + +;; That should be about it for most users... +;; unless you wanna hack elisp, the rest of this is probably uninteresting + + +;; ------------------------------------------------------------------------- +;; help determine what emacs we have here... + +(defconst promela-xemacsp (string-match "XEmacs" (emacs-version)) + "Non-nil if we are running in the XEmacs environment.") + +;;;(defconst promela-xemacs20p (and promela-xemacsp (>= emacs-major-version 20)) +;; "Non-nil if we are running in an XEmacs environment version 20 or greater.") + +;; ------------------------------------------------------------------------- +;; promela-mode font faces/definitions + +;; make use of font-lock stuff, so say that explicitly +(require 'font-lock) + +;; BLECH! YUCK! I just wish these guys could agree to something.... +;; Faces available in: ntemacs emacs xemacs xemacs xemacs +;; font-lock- xxx -face 20.6 19.34 19.16 20.x 21.x +;; -builtin- X +;; -constant- X +;; -comment- X X X X X +;; -doc-string- X X X +;; -function-name- X X X X X +;; -keyword- X X X X X +;; -preprocessor- X X X +;; -reference- X X X X +;; -signal-name- X X!20.0 +;; -string- X X X X X +;; -type- X X X X X +;; -variable-name- X X X X X +;; -warning- X X + +;;; Compatibility on faces between versions of emacs-en +(unless promela-xemacsp + + (defvar font-lock-preprocessor-face 'font-lock-preprocessor-face + "Face name to use for preprocessor statements.") + ;; For consistency try to define the preprocessor face == builtin face + (condition-case nil + (copy-face 'font-lock-builtin-face 'font-lock-preprocessor-face) + (error + (defface font-lock-preprocessor-face + '((t (:foreground "blue" :italic nil :underline t))) + "Face Lock mode face used to highlight preprocessor statements." + :group 'font-lock-highlighting-faces))) + + (defvar font-lock-reference-face 'font-lock-reference-face + "Face name to use for constants and reference and label names.") + ;; For consistency try to define the reference face == constant face + (condition-case nil + (copy-face 'font-lock-constant-face 'font-lock-reference-face) + (error + (defface font-lock-reference-face + '((((class grayscale) (background light)) + (:foreground "LightGray" :bold t :underline t)) + (((class grayscale) (background dark)) + (:foreground "Gray50" :bold t :underline t)) + (((class color) (background light)) (:foreground "CadetBlue")) + (((class color) (background dark)) (:foreground "Aquamarine")) + (t (:bold t :underline t))) + "Font Lock mode face used to highlight constancs, references and labels." + :group 'font-lock-highlighting-faces))) + + ) + +;; send-poll "symbol" face is custom to promela-mode +;; but check for existence to allow someone to override it +(defvar promela-fl-send-poll-face 'promela-fl-send-poll-face + "Face name to use for Promela Send or Poll symbols: `!' or `?'") +(copy-face (if promela-xemacsp 'modeline 'region) + 'promela-fl-send-poll-face) + +;; some emacs-en don't define or have regexp-opt available. +(unless (functionp 'regexp-opt) + (defmacro regexp-opt (strings) + "Cheap imitation of `regexp-opt' since it's not availble in this emacs" + `(mapconcat 'identity ,strings "\\|"))) + + +;; ------------------------------------------------------------------------- +;; promela-mode font lock specifications/regular-expressions +;; - for help, look at definition of variable 'font-lock-keywords +;; - some fontification ideas from -- [engstrom:20010309.1435CST] +;; Pat Tullman (tullmann@cs.utah.edu) and +;; Ny Aina Razermera Mamy (ainarazr@cs.uoregon.edu) +;; both had promela-mode's that I discovered after starting this one... +;; (but neither did any sort of indentation ;-) + +(defconst promela-font-lock-keywords-1 nil + "Subdued level highlighting for Promela mode.") + +(defconst promela-font-lock-keywords-2 nil + "Medium level highlighting for Promela mode.") + +(defconst promela-font-lock-keywords-3 nil + "Gaudy level highlighting for Promela mode.") + +;; set each of those three variables now.. +(let ((promela-keywords + (eval-when-compile + (regexp-opt + '("active" "assert" "atomic" "break" "d_step" + "do" "dproctype" "else" "empty" "enabled" + "eval" "fi" "full" "goto" "hidden" "if" "init" + "inline" "len" "local" "mtype" "nempty" "never" + "nfull" "od" "of" "pcvalue" "printf" "priority" + "proctype" "provided" "run" "show" "skip" + "timeout" "trace" "typedef" "unless" "xr" "xs")))) + (promela-types + (eval-when-compile + (regexp-opt '("bit" "bool" "byte" "short" + "int" "unsigned" "chan"))))) + + ;; really simple fontification (strings and comments come for "free") + (setq promela-font-lock-keywords-1 + (list + ;; Keywords: + (cons (concat "\\<\\(" promela-keywords "\\)\\>") + 'font-lock-keyword-face) + ;; Types: + (cons (concat "\\<\\(" promela-types "\\)\\>") + 'font-lock-type-face) + ;; Special constants: + '("\\<_\\(np\\|pid\\|last\\)\\>" . font-lock-reference-face))) + + ;; more complex fontification + ;; add function (proctype) names, lables and goto statements + ;; also add send/receive/poll fontification + (setq promela-font-lock-keywords-2 + (append promela-font-lock-keywords-1 + (list + ;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+") + '("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t) + + ;; "Functions" (proctype-s and inline-s) + (list (concat "\\<\\(" + (eval-when-compile + (regexp-opt '("run" "dproctype" "proctype" "inline"))) + "\\)\\>[ \t]*\\(\\sw+\\)?") + ;;'(1 'font-lock-keyword-face nil) + '(2 'font-lock-function-name-face nil t)) + + ;; Labels and GOTO labels + '("^\\(\\sw+\\):" 1 'font-lock-reference-face) + '("\\<\\(goto\\)\\>[ \t]+\\(\\sw+\\)" + ;;(1 'font-lock-keyword-face nil) + (2 'font-lock-reference-face nil t)) + + ;; Send, Receive and Poll + '("\\(\\sw+\\)\\(\\[[^\\?!]+\\]\\)?\\(\\??\\?\\|!?!\\)\\(\\sw+\\)" + (1 'font-lock-variable-name-face nil t) + (3 'promela-fl-send-poll-face nil t) + (4 'font-lock-reference-face nil t) + ) + ))) + + ;; most complex fontification + ;; add pre-processor directives, typed variables and hidden/typedef decls. + (setq promela-font-lock-keywords-3 + (append promela-font-lock-keywords-2 + (list + ;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+") + ;;'("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t) + ;; "defined" in an #if or #elif and associated macro names + '("^#[ \t]*\\(el\\)?if\\>" + ("\\<\\(defined\\)\\>[ \t]*(?\\(\\sw+\\)" nil nil + (1 'font-lock-preprocessor-face nil t) + (2 'font-lock-reference-face nil t))) + '("^#[ \t]*ifn?def\\>" + ("[ \t]*\\(\\sw+\\)" nil nil + (1 'font-lock-reference-face nil t))) + ;; Filenames in #include <...> directives + '("^#[ \t]*include[ \t]+<\\([^>\"\n]+\\)>" 1 'font-lock-string-face nil t) + ;; Defined functions and constants/types (non-functions) + '("^#[ \t]*define[ \t]+" + ("\\(\\sw+\\)(" nil nil (1 'font-lock-function-name-face nil t)) + ("\\(\\sw+\\)[ \t]+\\(\\sw+\\)" nil nil (1 'font-lock-variable-name-face) + (2 'font-lock-reference-face nil t)) + ("\\(\\sw+\\)[^(]?" nil nil (1 'font-lock-reference-face nil t))) + + ;; Types AND variables + ;; - room for improvement: (i.e. don't currently): + ;; highlight user-defined types and asociated variable declarations + (list (concat "\\<\\(" promela-types "\\)\\>") + ;;'(1 'font-lock-type-face) + ;; now match the variables after the type definition, if any + '(promela-match-variable-or-declaration + nil nil + (1 'font-lock-variable-name-face) ;; nil t) + (2 font-lock-reference-face nil t))) + + ;; Typedef/hidden types and declarations + '("\\<\\(typedef\\|hidden\\)\\>[ \t]*\\(\\sw+\\)?" + ;;(1 'font-lock-keyword-face nil) + (2 'font-lock-type-face nil t) + ;; now match the variables after the type definition, if any + (promela-match-variable-or-declaration + nil nil + (1 'font-lock-variable-name-face nil t) + (2 'font-lock-reference-face nil t))) + ))) + ) + +(defvar promela-font-lock-keywords promela-font-lock-keywords-1 + "Default expressions to highlight in Promela mode.") + +;; Font-lock matcher functions: +(defun promela-match-variable-or-declaration (limit) + "Match, and move over, any declaration/definition item after point. +Matches after point, but ignores leading whitespace characters. +Does not move further than LIMIT. + +The expected syntax of a declaration/definition item is `word' (preceded +by optional whitespace) optionally followed by a `= value' (preceded and +followed by more optional whitespace) + +Thus the regexp matches after point: word [ = value ] + ^^^^ ^^^^^ +Where the match subexpressions are: 1 2 + +The item is delimited by (match-beginning 1) and (match-end 1). +If (match-beginning 2) is non-nil, the item is followed by a `value'." + (when (looking-at "[ \t]*\\(\\sw+\\)[ \t]*=?[ \t]*\\(\\sw+\\)?[ \t]*,?") + (goto-char (min limit (match-end 0))))) + + +;; ------------------------------------------------------------------------- +;; "install" promela-mode font lock specifications + +;; FMI: look up 'font-lock-defaults +(defconst promela-font-lock-defaults + '( + (promela-font-lock-keywords + promela-font-lock-keywords-1 + promela-font-lock-keywords-2 + promela-font-lock-keywords-3) ;; font-lock stuff (keywords) + nil ;; keywords-only flag + nil ;; case-fold keyword searching + ;;((?_ . "w") (?$ . ".")) ;; mods to syntax table + nil ;; mods to syntax table (see below) + nil ;; syntax-begin + (font-lock-mark-block-function . mark-defun)) +) + +;; "install" the font-lock-defaults based upon version of emacs we have +(cond (promela-xemacsp + (put 'promela-mode 'font-lock-defaults promela-font-lock-defaults)) + ((not (assq 'promela-mode font-lock-defaults-alist)) + (setq font-lock-defaults-alist + (cons + (cons 'promela-mode promela-font-lock-defaults) + font-lock-defaults-alist)))) + + +;; ------------------------------------------------------------------------- +;; other promela-mode specific definitions + +(defconst promela-defun-prompt-regexp + "^[ \t]*\\(d?proctype\\|init\\|inline\\|never\\|trace\\|typedef\\|mtype\\s-+=\\)[^{]*" + "Regexp describing the beginning of a Promela top-level definition.") + +(defvar promela-mode-syntax-table nil + "Syntax table in use in PROMELA-mode buffers.") +(if promela-mode-syntax-table + () + (setq promela-mode-syntax-table (make-syntax-table)) + (modify-syntax-entry ?\\ "\\" promela-mode-syntax-table) + (modify-syntax-entry ?/ ". 14" promela-mode-syntax-table) + (modify-syntax-entry ?* ". 23" promela-mode-syntax-table) + (modify-syntax-entry ?+ "." promela-mode-syntax-table) + (modify-syntax-entry ?- "." promela-mode-syntax-table) + (modify-syntax-entry ?= "." promela-mode-syntax-table) + (modify-syntax-entry ?% "." promela-mode-syntax-table) + (modify-syntax-entry ?< "." promela-mode-syntax-table) + (modify-syntax-entry ?> "." promela-mode-syntax-table) + (modify-syntax-entry ?& "." promela-mode-syntax-table) + (modify-syntax-entry ?| "." promela-mode-syntax-table) + (modify-syntax-entry ?. "_" promela-mode-syntax-table) + (modify-syntax-entry ?_ "w" promela-mode-syntax-table) + (modify-syntax-entry ?\' "\"" promela-mode-syntax-table) + ) + +(defvar promela-mode-abbrev-table nil + "*Abbrev table in use in promela-mode buffers.") +(if promela-mode-abbrev-table + nil + (define-abbrev-table 'promela-mode-abbrev-table + '( +;; Commented out for now - need to think about what abbrevs make sense +;; ("assert" "ASSERT" promela-check-expansion 0) +;; ("d_step" "D_STEP" promela-check-expansion 0) +;; ("break" "BREAK" promela-check-expansion 0) +;; ("do" "DO" promela-check-expansion 0) +;; ("proctype" "PROCTYPE" promela-check-expansion 0) + ))) + +(defvar promela-mode-map nil + "Keymap for promela-mode.") +(if promela-mode-map + nil + (setq promela-mode-map (make-sparse-keymap)) + (define-key promela-mode-map "\t" 'promela-indent-command) + (define-key promela-mode-map "\C-m" 'promela-newline-and-indent) + ;(define-key promela-mode-map 'backspace 'backward-delete-char-untabify) + (define-key promela-mode-map "\C-c\C-p" 'promela-beginning-of-block) + ;(define-key promela-mode-map "\C-c\C-n" 'promela-end-of-block) + (define-key promela-mode-map "\M-\C-a" 'promela-beginning-of-defun) + ;(define-key promela-mode-map "\M-\C-e" 'promela-end-of-defun) + (define-key promela-mode-map "\C-c(" 'promela-toggle-auto-match-delimiter) + (define-key promela-mode-map "{" 'promela-open-delimiter) + (define-key promela-mode-map "}" 'promela-close-delimiter) + (define-key promela-mode-map "(" 'promela-open-delimiter) + (define-key promela-mode-map ")" 'promela-close-delimiter) + (define-key promela-mode-map "[" 'promela-open-delimiter) + (define-key promela-mode-map "]" 'promela-close-delimiter) + (define-key promela-mode-map ";" 'promela-insert-and-indent) + (define-key promela-mode-map ":" 'promela-insert-and-indent) + ;; + ;; this is preliminary at best - use at your own risk: + (define-key promela-mode-map "\C-c\C-s" 'promela-syntax-check) + ;; + ;;(define-key promela-mode-map "\C-c\C-d" 'promela-mode-toggle-debug) + ;;(define-key promela-mode-map "\C-c\C-r" 'promela-mode-revert-buffer) + ) + +(defvar promela-matching-delimiter-alist + '( (?( . ?)) + (?[ . ?]) + (?{ . "\n}") + ;(?< . ?>) + (?\' . ?\') + (?\` . ?\`) + (?\" . ?\") ) + "List of pairs of matching open/close delimiters - for auto-insert") + + +;; ------------------------------------------------------------------------- +;; Promela-mode itself + +(defun promela-mode () + "Major mode for editing PROMELA code. +\\{promela-mode-map} + +Variables controlling indentation style: + promela-block-indent + Relative offset of lines within a block (`{') construct. + + promela-selection-indent + Relative offset of option lines within a selection (`if') + or iteration (`do') construct. + + promela-selection-option-indent + Relative offset of lines after/within options (`::') within + selection or iteration constructs. + + promela-comment-col + Defines the desired comment column for comments to the right of text. + + promela-tab-always-indent + Non-nil means TAB in PROMELA mode should always reindent the current + line, regardless of where in the line the point is when the TAB + command is used. + + promela-auto-match-delimiter + Non-nil means typing an open-delimiter (i.e. parentheses, brace, + quote, etc) should also insert the matching closing delmiter + character. + +Turning on PROMELA mode calls the value of the variable promela-mode-hook with +no args, if that value is non-nil. + +For example: ' + (setq promela-mode-hook '(lambda () + (setq promela-block-indent 2) + (setq promela-selection-indent 0) + (setq promela-selection-option-indent 2) + (local-set-key \"\\C-m\" 'promela-indent-newline-indent) + ))' + +will indent block two steps, will make selection options aligned with DO/IF +and sub-option lines indent to a column after the `::'. Also, lines will +be reindented when you hit RETURN. + +Note that promela-mode adhears to the font-lock \"standards\" and +defines several \"levels\" of fontification or colorization. The +default is fairly gaudy, so if you would prefer a bit less, please see +the documentation for the variable: `font-lock-maximum-decoration'. +" + (interactive) + (kill-all-local-variables) + (setq mode-name "Promela") + (setq major-mode 'promela-mode) + (use-local-map promela-mode-map) + (set-syntax-table promela-mode-syntax-table) + (setq local-abbrev-table promela-mode-abbrev-table) + + ;; Make local variables + (make-local-variable 'case-fold-search) + (make-local-variable 'paragraph-start) + (make-local-variable 'paragraph-separate) + (make-local-variable 'paragraph-ignore-fill-prefix) + (make-local-variable 'indent-line-function) + (make-local-variable 'indent-region-function) + (make-local-variable 'parse-sexp-ignore-comments) + (make-local-variable 'comment-start) + (make-local-variable 'comment-end) + (make-local-variable 'comment-column) + (make-local-variable 'comment-start-skip) + (make-local-variable 'comment-indent-hook) + (make-local-variable 'defun-prompt-regexp) + (make-local-variable 'compile-command) + ;; Now set their values + (setq case-fold-search t + paragraph-start (concat "^$\\|" page-delimiter) + paragraph-separate paragraph-start + paragraph-ignore-fill-prefix t + indent-line-function 'promela-indent-command + ;;indent-region-function 'promela-indent-region + parse-sexp-ignore-comments t + comment-start "/* " + comment-end " */" + comment-column 32 + comment-start-skip "/\\*+ *" + ;;comment-start-skip "/\\*+ *\\|// *" + ;;comment-indent-hook 'promela-comment-indent + defun-prompt-regexp promela-defun-prompt-regexp + ) + + ;; Turn on font-lock mode + ;; (and promela-font-lock-mode (font-lock-mode)) + (font-lock-mode) + + ;; Finally, run the hooks and be done. + (run-hooks 'promela-mode-hook)) + + +;; ------------------------------------------------------------------------- +;; Interactive functions +;; + +(defun promela-mode-version () + "Print the current version of promela-mode in the minibuffer" + (interactive) + (message (concat "Promela-Mode: " promela-mode-version))) + +(defun promela-beginning-of-block () + "Move backward to start of containing block. +Containing block may be `{', `do' or `if' construct, or comment." + (interactive) + (goto-char (promela-find-start-of-containing-block-or-comment))) + +(defun promela-beginning-of-defun (&optional arg) + "Move backward to the beginning of a defun. +With argument, do it that many times. +Negative arg -N means move forward to Nth following beginning of defun. +Returns t unless search stops due to beginning or end of buffer. + +See also 'beginning-of-defun. + +This is a Promela-mode specific version since default (in xemacs 19.16 and +NT-Emacs 20) don't seem to skip comments - they will stop inside them. + +Also, this makes sure that the beginning of the defun is actually the +line which starts the proctype/init/etc., not just the open-brace." + (interactive "p") + (beginning-of-defun arg) + (if (not (looking-at promela-defun-prompt-regexp)) + (re-search-backward promela-defun-prompt-regexp nil t)) + (if (promela-inside-comment-p) + (goto-char (promela-find-start-of-containing-comment)))) + +(defun promela-indent-command () + "Indent the current line as PROMELA code." + (interactive) + (if (and (not promela-tab-always-indent) + (save-excursion + (skip-chars-backward " \t") + (not (bolp)))) + (tab-to-tab-stop) + (promela-indent-line))) + +(defun promela-newline-and-indent () + "Promela-mode specific newline-and-indent which expands abbrevs before +running a regular newline-and-indent." + (interactive) + (if abbrev-mode + (expand-abbrev)) + (newline-and-indent)) + +(defun promela-indent-newline-indent () + "Promela-mode specific newline-and-indent which expands abbrevs and +indents the current line before running a regular newline-and-indent." + (interactive) + (save-excursion (promela-indent-command)) + (if abbrev-mode + (expand-abbrev)) + (newline-and-indent)) + +(defun promela-insert-and-indent () + "Insert the last character typed and re-indent the current line" + (interactive) + (insert last-command-char) + (save-excursion (promela-indent-command))) + +(defun promela-open-delimiter () + "Inserts the open and matching close delimiters, indenting as appropriate." + (interactive) + (insert last-command-char) + (if (and promela-auto-match-delimiter (not (promela-inside-comment-p))) + (save-excursion + (insert (cdr (assq last-command-char promela-matching-delimiter-alist))) + (promela-indent-command)))) + +(defun promela-close-delimiter () + "Inserts and indents a close delimiter." + (interactive) + (insert last-command-char) + (if (not (promela-inside-comment-p)) + (save-excursion (promela-indent-command)))) + +(defun promela-toggle-auto-match-delimiter () + "Toggle auto-insertion of parens and other delimiters. +See variable `promela-auto-insert-matching-delimiter'" + (interactive) + (setq promela-auto-match-delimiter + (not promela-auto-match-delimiter)) + (message (concat "Promela auto-insert matching delimiters " + (if promela-auto-match-delimiter + "enabled" "disabled")))) + + +;; ------------------------------------------------------------------------- +;; Compilation/Verification functions + +;; all of this is in serious "beta" mode - don't trust it ;-) +(setq + promela-compile-command "spin " + promela-syntax-check-args "-a -v " +) + +;;(setq compilation-error-regexp-alist +;; (append compilation-error-regexp-alist +;; '(("spin: +line +\\([0-9]+\\) +\"\\([^\"]+\\)\"" 2 1)))) + +(defun promela-syntax-check () + (interactive) + (compile (concat promela-compile-command + promela-syntax-check-args + (buffer-name)))) + + +;; ------------------------------------------------------------------------- +;; Indentation support functions + +(defun promela-indent-around-label () + "Indent the current line as PROMELA code, +but make sure to consider the label at the beginning of the line." + (beginning-of-line) + (delete-horizontal-space) ; delete any leading whitespace + (if (not (looking-at "\\sw+:\\([ \t]*\\)")) + (error "promela-indent-around-label: no label on this line") + (goto-char (match-beginning 1)) + (let* ((space (length (match-string 1))) + (indent (promela-calc-indent)) + (wanted (max 0 (- indent (current-column))))) + (if (>= space wanted) + (delete-region (point) (+ (point) (- space wanted))) + (goto-char (+ (point) space)) + (indent-to-column indent))))) + +;; Note that indentation is based ENTIRELY upon the indentation of the +;; previous line(s), esp. the previous non-blank line and the line +;; starting the current containgng block... +(defun promela-indent-line () + "Indent the current line as PROMELA code. +Return the amount the by which the indentation changed." + (beginning-of-line) + (if (looking-at "[ \t]*\\sw+:") + (promela-indent-around-label) + (let ((indent (promela-calc-indent)) + beg + shift-amt + (pos (- (point-max) (point)))) + (setq beg (point)) + (skip-chars-forward " \t") + (setq shift-amt (- indent (current-column))) + (if (zerop shift-amt) + (if (> (- (point-max) pos) (point)) + (goto-char (- (point-max) pos))) + (delete-region beg (point)) + (indent-to indent) + (if (> (- (point-max) pos) (point)) + (goto-char (- (point-max) pos)))) + shift-amt))) + +(defun promela-calc-indent () + "Return the appropriate indentation for this line as an int." + (save-excursion + (beginning-of-line) + (let* ((orig-point (point)) + (state (promela-parse-partial-sexp)) + (paren-depth (nth 0 state)) + (paren-point (or (nth 1 state) 1)) + (paren-char (char-after paren-point))) + ;;(what-cursor-position) + (cond + ;; Indent not-at-all - inside a string + ((nth 3 state) + (current-indentation)) + ;; Indent inside a comment + ((nth 4 state) + (promela-calc-indent-within-comment)) + ;; looking at a pre-processor directive - indent=0 + ((looking-at "[ \t]*#\\(define\\|if\\(n?def\\)?\\|else\\|endif\\)") + 0) + ;; If we're not inside a "true" block (i.e. "{}"), then indent=0 + ;; I think this is fair, since no (indentable) code in promela + ;; exists outside of a proctype or similar "{ .. }" structure. + ((zerop paren-depth) + 0) + ;; Indent relative to non curly-brace "paren" + ;; [ NOTE: I'm saving this, but don't use it any more. + ;; Now, we let parens be indented like curly braces + ;;((and (>= paren-depth 1) (not (char-equal ?\{ paren-char))) + ;; (goto-char paren-point) + ;; (1+ (current-column))) + ;; + ;; Last option: indent relative to contaning block(s) + (t + (goto-char orig-point) + (promela-calc-indent-within-block paren-point)))))) + +(defun promela-calc-indent-within-block (&optional limit) + "Return the appropriate indentation for this line, assume within block. +with optional arg, limit search back to `limit'" + (save-excursion + (let* ((stop (or limit 1)) + (block-point (promela-find-start-of-containing-block stop)) + (block-type (promela-block-type-after block-point)) + (indent-point (point)) + (indent-type (promela-block-type-after indent-point))) + (if (not block-type) 0 + ;;(message "paren: %d (%d); block: %s (%d); indent: %s (%d); stop: %d" + ;; paren-depth paren-point block-type block-point + ;; indent-type indent-point stop) + (goto-char block-point) + (cond + ;; Indent (options) inside "if" or "do" + ((memq block-type '(selection iteration)) + (if (re-search-forward "\\(do\\|if\\)[ \t]*::" indent-point t) + (- (current-column) 2) + (+ (current-column) promela-selection-indent))) + ;; indent (generic code) inside "::" option + ((eq 'option block-type) + (if (and (not indent-type) + (re-search-forward "::.*->[ \t]*\\sw" + (save-excursion (end-of-line) (point)) + t)) + (1- (current-column)) + (+ (current-column) promela-selection-option-indent)) + ) + ;; indent code inside "{" + ((eq 'block block-type) + (cond + ;; if we are indenting the end of a block, + ;; use indentation of start-of-block + ((equal 'block-end indent-type) + (current-indentation)) + ;; if the start of the code inside the block is not at eol + ;; then indent to the same column as the block start +some + ;; [ but ignore comments after "{" ] + ((and (not (promela-effective-eolp (1+ (point)))) + (not (looking-at "{[ \t]*/\\*"))) + (forward-char) ; skip block-start + (skip-chars-forward "{ \t") ; skip whitespace, if any + (current-column)) + ;; anything else we indent +promela-block-indent from + ;; the indentation of the start of block (where we are now) + (t + (+ (current-indentation) + promela-block-indent)))) + ;; dunno what kind of block this is - sound an error + (t + (error "promela-calc-indent-within-block: unknown block type: %s" block-type) + (current-indentation))))))) + +(defun promela-calc-indent-within-comment () + "Return the indentation amount for line, assuming that the +current line is to be regarded as part of a block comment." + (save-excursion + (beginning-of-line) + (skip-chars-forward " \t") + (let ((indenting-end-of-comment (looking-at "\\*/")) + (indenting-blank-line (eolp))) + ;; if line is NOT blank and next char is NOT a "*' + (if (not (or indenting-blank-line (= (following-char) ?\*))) + ;; leave indent alone + (current-column) + ;; otherwise look back for _PREVIOUS_ possible nested comment start + (let ((comment-start (save-excursion + (re-search-backward comment-start-skip)))) + ;; and see if there is an appropriate middle-comment "*" + (if (re-search-backward "^[ \t]+\\*" comment-start t) + (current-indentation) + ;; guess not, so indent relative to comment start + (goto-char comment-start) + (if indenting-end-of-comment + (current-column) + (1+ (current-column))))))))) + + +;; ------------------------------------------------------------------------- +;; Misc other support functions + +(defun promela-parse-partial-sexp (&optional start limit) + "Return the partial parse state of current defun or from optional start +to end limit" + (save-excursion + (let ((end (or limit (point)))) + (if start + (goto-char start) + (promela-beginning-of-defun)) + (parse-partial-sexp (point) end)))) + +;;(defun promela-at-end-of-block-p () +;; "Return t if cursor is at the end of a promela block" +;; (save-excursion +;; (let ((eol (progn (end-of-line) (point)))) +;; (beginning-of-line) +;; (skip-chars-forward " \t") +;; ;;(re-search-forward "\\(}\\|\\b\\(od\\|fi\\)\\b\\)" eol t)))) +;; (looking-at "[ \t]*\\(od\\|fi\\)\\b")))) + +(defun promela-inside-comment-p () + "Check if the point is inside a comment block." + (save-excursion + (let ((origpoint (point)) + state) + (goto-char 1) + (while (> origpoint (point)) + (setq state (parse-partial-sexp (point) origpoint 0))) + (nth 4 state)))) + +(defun promela-inside-comment-or-string-p () + "Check if the point is inside a comment or a string." + (save-excursion + (let ((origpoint (point)) + state) + (goto-char 1) + (while (> origpoint (point)) + (setq state (parse-partial-sexp (point) origpoint 0))) + (or (nth 3 state) (nth 4 state))))) + + +(defun promela-effective-eolp (&optional point) + "Check if we are at the effective end-of-line, ignoring whitespace" + (save-excursion + (if point (goto-char point)) + (skip-chars-forward " \t") + (eolp))) + +(defun promela-check-expansion () + "If abbrev was made within a comment or a string, de-abbrev!" + (if promela-inside-comment-or-string-p + (unexpand-abbrev))) + +(defun promela-block-type-after (&optional point) + "Return the type of block after current point or parameter as a symbol. +Return one of 'iteration `do', 'selection `if', 'option `::', +'block `{' or `}' or nil if none of the above match." + (save-excursion + (goto-char (or point (point))) + (skip-chars-forward " \t") + (cond + ((looking-at "do\\b") 'iteration) + ;;((looking-at "od\\b") 'iteration-end) + ((looking-at "if\\b") 'selection) + ;;((looking-at "fi\\b") 'selection-end) + ((looking-at "::") 'option) + ((looking-at "[{(]") 'block) + ((looking-at "[})]") 'block-end) + (t nil)))) + +(defun promela-find-start-of-containing-comment (&optional limit) + "Return the start point of the containing comment block. +Stop at `limit' or beginning of buffer." + (let ((stop (or limit 1))) + (save-excursion + (while (and (>= (point) stop) + (nth 4 (promela-parse-partial-sexp))) + (re-search-backward comment-start-skip stop t)) + (point)))) + +(defun promela-find-start-of-containing-block (&optional limit) + "Return the start point of the containing `do', `if', `::' or +`{' block or containing comment. +Stop at `limit' or beginning of buffer." + (save-excursion + (skip-chars-forward " \t") + (let* ((type (promela-block-type-after)) + (stop (or limit + (save-excursion (promela-beginning-of-defun) (point)))) + (state (promela-parse-partial-sexp stop)) + (level (if (looking-at "\\(od\\|fi\\)\\b") + 2 + (if (zerop (nth 0 state)) 0 1)))) + ;;(message "find-start-of-containing-block: type: %s; level %d; stop %d" + ;; type level stop) + (while (and (> (point) stop) (not (zerop level))) + (re-search-backward + "\\({\\|}\\|::\\|\\b\\(do\\|od\\|if\\|fi\\)\\b\\)" + stop 'move) + ;;(message "looking from %d back-to %d" (point) stop) + (setq state (promela-parse-partial-sexp stop)) + (setq level (+ level + (cond ((or (nth 3 state) (nth 4 state)) 0) + ((and (= 1 level) (looking-at "::") + (not (equal type 'option))) -1) + ((looking-at "\\({\\|\\(do\\|if\\)\\b\\)") -1) + ((looking-at "\\(}\\|\\(od\\|fi\\)\\b\\)") +1) + (t 0))))) + (point)))) + +(defun promela-find-start-of-containing-block-or-comment (&optional limit) + "Return the start point of the containing comment or +the start of the containing `do', `if', `::' or `{' block. +Stop at limit or beginning of buffer." + (if (promela-inside-comment-p) + (promela-find-start-of-containing-comment limit) + (promela-find-start-of-containing-block limit))) + +;; ------------------------------------------------------------------------- +;; Debugging/testing + +;; (defun promela-mode-toggle-debug () +;; (interactive) +;; (make-local-variable 'debug-on-error) +;; (setq debug-on-error (not debug-on-error))) + +;;(defun promela-mode-revert-buffer () +;; (interactive) +;; (revert-buffer t t)) + +;; ------------------------------------------------------------------------- +;;###autoload + +(provide 'promela-mode) + + +;;---------------------------------------------------------------------- +;; Change History: +;; +;; $Log: promela-mode.el,v $ +;; Revision 1.11 2001/07/09 18:36:45 engstrom +;; - added comments on use of font-lock-maximum-decoration +;; - moved basic preprocess directive fontification to "level 2" +;; +;; Revision 1.10 2001/05/22 16:29:59 engstrom +;; - fixed error introduced in fontification levels stuff (xemacs only) +;; +;; Revision 1.9 2001/05/22 16:21:29 engstrom +;; - commented out the compilation / syntax check stuff for now +;; +;; Revision 1.8 2001/05/22 16:18:49 engstrom +;; - Munched history in preparation for first non-Honeywell release +;; - Added "levels" of fontification to be controlled by the std. variable: +;; 'font-lock-maximum-decoration' +;; +;; Revision 1.7 2001/04/20 01:41:46 engstrom +;; Revision 1.6 2001/04/06 23:57:18 engstrom +;; Revision 1.5 2001/04/04 20:04:15 engstrom +;; Revision 1.4 2001/03/15 02:22:18 engstrom +;; Revision 1.3 2001/03/09 19:39:51 engstrom +;; Revision 1.2 2001/03/01 18:07:47 engstrom +;; Revision 1.1 2001/02/01 xx:xx:xx engstrom +;; migrated to CVS versioning... +;; Pre-CVS-History: +;; 99-10-04 V0.4 EDE Fixed bug in end-of-block indentation +;; Simplified indentation code significantly +;; 99-09-2x V0.3 EDE Hacked on indentation more while at FM'99 +;; 99-09-16 V0.2 EDE Hacked, hacked, hacked on indentation +;; 99-04-01 V0.1 EDE Introduced (less-than) half-baked indentation +;; 98-11-05 V0.0 EDE Created - much code stolen from rexx-mode.el +;; Mostly just a fontification mode - +;; (indentation is HARD ;-) +;; +;; EOF promela-mode.el -- 2.39.5