174675a66SBram Moolenaar" Vim syntax file 274675a66SBram Moolenaar" Language: Murphi model checking language 374675a66SBram Moolenaar" Maintainer: Matthew Fernandez <[email protected]> 4*06fe74aeSBram Moolenaar" Last Change: 2019 Aug 27 574675a66SBram Moolenaar" Version: 2 674675a66SBram Moolenaar" Remark: Originally authored by Diego Ongaro <[email protected]> 774675a66SBram Moolenaar 874675a66SBram Moolenaarif version < 600 974675a66SBram Moolenaar syntax clear 1074675a66SBram Moolenaarelseif exists("b:current_syntax") 1174675a66SBram Moolenaar finish 1274675a66SBram Moolenaarendif 1374675a66SBram Moolenaar 1474675a66SBram Moolenaar" Keywords are case insensitive. 1574675a66SBram Moolenaar" Keep these in alphabetical order. 1674675a66SBram Moolenaarsyntax case ignore 1774675a66SBram Moolenaarsyn keyword murphiKeyword alias 1874675a66SBram Moolenaarsyn keyword murphiStructure array 1974675a66SBram Moolenaarsyn keyword murphiKeyword assert 2074675a66SBram Moolenaarsyn keyword murphiKeyword begin 2174675a66SBram Moolenaarsyn keyword murphiType boolean 2274675a66SBram Moolenaarsyn keyword murphiKeyword by 2374675a66SBram Moolenaarsyn keyword murphiLabel case 2474675a66SBram Moolenaarsyn keyword murphiKeyword clear 2574675a66SBram Moolenaarsyn keyword murphiLabel const 2674675a66SBram Moolenaarsyn keyword murphiRepeat do 2774675a66SBram Moolenaarsyn keyword murphiConditional else 2874675a66SBram Moolenaarsyn keyword murphiConditional elsif 2974675a66SBram Moolenaarsyn keyword murphiKeyword end 3074675a66SBram Moolenaarsyn keyword murphiKeyword endalias 3174675a66SBram Moolenaarsyn keyword murphiRepeat endexists 3274675a66SBram Moolenaarsyn keyword murphiRepeat endfor 3374675a66SBram Moolenaarsyn keyword murphiRepeat endforall 3474675a66SBram Moolenaarsyn keyword murphiKeyword endfunction 3574675a66SBram Moolenaarsyn keyword murphiConditional endif 3674675a66SBram Moolenaarsyn keyword murphiKeyword endprocedure 3774675a66SBram Moolenaarsyn keyword murphiStructure endrecord 3874675a66SBram Moolenaarsyn keyword murphiKeyword endrule 3974675a66SBram Moolenaarsyn keyword murphiKeyword endruleset 4074675a66SBram Moolenaarsyn keyword murphiKeyword endstartstate 4174675a66SBram Moolenaarsyn keyword murphiConditional endswitch 4274675a66SBram Moolenaarsyn keyword murphiRepeat endwhile 4374675a66SBram Moolenaarsyn keyword murphiStructure enum 4474675a66SBram Moolenaarsyn keyword murphiKeyword error 4574675a66SBram Moolenaarsyn keyword murphiRepeat exists 4674675a66SBram Moolenaarsyn keyword murphiBoolean false 4774675a66SBram Moolenaarsyn keyword murphiRepeat for 4874675a66SBram Moolenaarsyn keyword murphiRepeat forall 4974675a66SBram Moolenaarsyn keyword murphiKeyword function 5074675a66SBram Moolenaarsyn keyword murphiConditional if 5174675a66SBram Moolenaarsyn keyword murphiKeyword in 5274675a66SBram Moolenaarsyn keyword murphiKeyword interleaved 5374675a66SBram Moolenaarsyn keyword murphiLabel invariant 5474675a66SBram Moolenaarsyn keyword murphiFunction ismember 5574675a66SBram Moolenaarsyn keyword murphiFunction isundefined 5674675a66SBram Moolenaarsyn keyword murphiKeyword log 5774675a66SBram Moolenaarsyn keyword murphiStructure of 5874675a66SBram Moolenaarsyn keyword murphiType multiset 5974675a66SBram Moolenaarsyn keyword murphiFunction multisetadd 6074675a66SBram Moolenaarsyn keyword murphiFunction multisetcount 6174675a66SBram Moolenaarsyn keyword murphiFunction multisetremove 6274675a66SBram Moolenaarsyn keyword murphiFunction multisetremovepred 6374675a66SBram Moolenaarsyn keyword murphiKeyword procedure 6474675a66SBram Moolenaarsyn keyword murphiKeyword program 6574675a66SBram Moolenaarsyn keyword murphiKeyword put 6674675a66SBram Moolenaarsyn keyword murphiStructure record 6774675a66SBram Moolenaarsyn keyword murphiKeyword return 6874675a66SBram Moolenaarsyn keyword murphiLabel rule 6974675a66SBram Moolenaarsyn keyword murphiLabel ruleset 7074675a66SBram Moolenaarsyn keyword murphiType scalarset 7174675a66SBram Moolenaarsyn keyword murphiLabel startstate 7274675a66SBram Moolenaarsyn keyword murphiConditional switch 7374675a66SBram Moolenaarsyn keyword murphiConditional then 7474675a66SBram Moolenaarsyn keyword murphiRepeat to 7574675a66SBram Moolenaarsyn keyword murphiKeyword traceuntil 7674675a66SBram Moolenaarsyn keyword murphiBoolean true 7774675a66SBram Moolenaarsyn keyword murphiLabel type 7874675a66SBram Moolenaarsyn keyword murphiKeyword undefine 7974675a66SBram Moolenaarsyn keyword murphiStructure union 8074675a66SBram Moolenaarsyn keyword murphiLabel var 8174675a66SBram Moolenaarsyn keyword murphiRepeat while 8274675a66SBram Moolenaar 8374675a66SBram Moolenaarsyn keyword murphiTodo contained todo xxx fixme 8474675a66SBram Moolenaarsyntax case match 8574675a66SBram Moolenaar 8674675a66SBram Moolenaar" Integers. 8774675a66SBram Moolenaarsyn match murphiNumber "\<\d\+\>" 8874675a66SBram Moolenaar 8974675a66SBram Moolenaar" Operators and special characters. 9074675a66SBram Moolenaarsyn match murphiOperator "[\+\-\*\/%&|=!<>:\?]\|\." 91*06fe74aeSBram Moolenaarsyn match murphiDelimiter "\(:=\@!\|[;,]\)" 9274675a66SBram Moolenaarsyn match murphiSpecial "[()\[\]]" 9374675a66SBram Moolenaar 9474675a66SBram Moolenaar" Double equal sign is a common error: use one equal sign for equality testing. 9574675a66SBram Moolenaarsyn match murphiError "==[^>]"he=e-1 9674675a66SBram Moolenaar" Double && and || are errors. 9774675a66SBram Moolenaarsyn match murphiError "&&\|||" 9874675a66SBram Moolenaar 9974675a66SBram Moolenaar" Strings. This is defined so late so that it overrides previous matches. 10074675a66SBram Moolenaarsyn region murphiString start=+"+ end=+"+ 10174675a66SBram Moolenaar 10274675a66SBram Moolenaar" Comments. This is defined so late so that it overrides previous matches. 10374675a66SBram Moolenaarsyn region murphiComment start="--" end="$" contains=murphiTodo 10474675a66SBram Moolenaarsyn region murphiComment start="/\*" end="\*/" contains=murphiTodo 10574675a66SBram Moolenaar 10674675a66SBram Moolenaar" Link the rules to some groups. 107c572da5fSBram Moolenaarhi def link murphiComment Comment 108c572da5fSBram Moolenaarhi def link murphiString String 109c572da5fSBram Moolenaarhi def link murphiNumber Number 110c572da5fSBram Moolenaarhi def link murphiBoolean Boolean 111c572da5fSBram Moolenaarhi def link murphiIdentifier Identifier 112c572da5fSBram Moolenaarhi def link murphiFunction Function 113c572da5fSBram Moolenaarhi def link murphiStatement Statement 114c572da5fSBram Moolenaarhi def link murphiConditional Conditional 115c572da5fSBram Moolenaarhi def link murphiRepeat Repeat 116c572da5fSBram Moolenaarhi def link murphiLabel Label 117c572da5fSBram Moolenaarhi def link murphiOperator Operator 118c572da5fSBram Moolenaarhi def link murphiKeyword Keyword 119c572da5fSBram Moolenaarhi def link murphiType Type 120c572da5fSBram Moolenaarhi def link murphiStructure Structure 121c572da5fSBram Moolenaarhi def link murphiSpecial Special 122c572da5fSBram Moolenaarhi def link murphiDelimiter Delimiter 123c572da5fSBram Moolenaarhi def link murphiError Error 124c572da5fSBram Moolenaarhi def link murphiTodo Todo 12574675a66SBram Moolenaar 12674675a66SBram Moolenaarlet b:current_syntax = "murphi" 127