--- /dev/null
+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}
+}
+
+
--- /dev/null
+;; 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 <eric.engstrom@honeywell.com>
+;; 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 ]
+\f
+;;; -------------------------------------------------------------------------
+;;; 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
+
+\f
+;; -------------------------------------------------------------------------
+;; 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 "\\|")))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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)))))
+
+\f
+;; -------------------------------------------------------------------------
+;; "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))))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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")
+
+\f
+;; -------------------------------------------------------------------------
+;; 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))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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"))))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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))))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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)))))))))
+
+\f
+;; -------------------------------------------------------------------------
+;; 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)
+
+\f
+;;----------------------------------------------------------------------
+;; 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
