045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyDescription : Isabelle Abstract syntax constants for CSP-Prover operations
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillyCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly Swansea University 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyMaintainer : csliam@swansea.ac.uk
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyStability : provisional
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyPortability : portable
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyIsabelle Abstract syntax constants for CSP-Prover operations.
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_skipOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_stopOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_divOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_runOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_chaosOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceOp,
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_sequenceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_external_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_internal_choiceOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_interleavingOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_synchronousOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_general_parallelOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_hidingOp,
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_renamingOp,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cspProver_conditionalOp,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cspProver_chan_nondeterministic_sendOp
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reillyimport Isabelle.IsaSign as IsaSign
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reillyimport Isabelle.IsaConsts (binVNameAppl, con, termAppl)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Symbols for CspProver
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThese symbols and priorities have come from the CSP-Prover source code -}
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- SKIP primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipS = "SKIP"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- STOP primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopS = "STOP"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- DIV primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divS = "DIV"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- RUN primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runS = "??? RUN ??? - NOT YET DONE"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- CHAOS primitive process symbol
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Action prefix operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_action_prefixS = "Act_prefix"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltS = "(_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_action_prefixAltArgPrios = [150, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- External prefix choice operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_external_prefix_choiceS = "Ext_pre_choice"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltS = "(? _:_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_external_prefix_choiceAltArgPrios = [900, 900, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Internal prefix choice operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_internal_prefix_choiceS = "Int_pre_choice"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltS :: String
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltS = "(! _:_ -> _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_internal_prefix_choiceAltArgPrios = [900, 900, 80]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceAltOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Sequence combinator operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceS = "Seq_compo"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltS = "(_ ;; _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_sequenceAltArgPrios = [79, 78]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceAltOpPrio = 78
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- External choice operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_external_choiceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceS = "Ext_choice"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltS = "( _ [+] _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_external_choiceAltArgPrios = [72, 73]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceAltOpPrio = 72
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Internal choice operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_internal_choiceS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceS = "Int_choice"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltS = "(_ |~| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_internal_choiceAltArgPrios = [64, 65]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceAltOpPrio = 64
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Interleaving parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingS = "Interleave"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltS = "(_ ||| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_interleavingAltArgPrios = [76, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Synchronous parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousS = "Synchro"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltS = "(_ || _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_synchronousAltArgPrios = [76, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Generalised parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelS :: String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_general_parallelS = "Parallel"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltS = "(_ |[_]| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_general_parallelAltArgPrios = [76, 0, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Alphabetised parallel operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelS = "Alpha_parallel"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltS = "(_ |[_,_]| _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_alphabetised_parallelAltArgPrios = [76, 0, 0, 77]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelAltOpPrio = 76
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Hiding operator symbols
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillycspProver_hidingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingS = "Hiding"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltS = "(_ -- _)"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_hidingAltArgPrios = [84, 85]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingAltOpPrio = 85
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Renaming operator symbols
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingS = "Renaming"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltS :: String
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltS = "(_ [[_]])"
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_renamingAltArgPrios = [84, 0]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltOpPrio :: Int
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingAltOpPrio = 84
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Conditional operator symbols
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalS :: String
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillycspProver_conditionalS = "IF"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltS :: String
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillycspProver_conditionalAltS = "(IF _ THEN _ ELSE _)"
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_conditionalAltArgPrios = [900, 88, 88]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgOpPrio :: Int
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalAltArgOpPrio = 88
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Channel Non-deterministic send operator symbols
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederOnly works if pretty printed using the alternative syntax -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendS = "Nondet_send_prefix"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltS = "(_ !? _:_ -> _)"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgPrios :: [Int]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_chan_nondeterministic_sendAltArgPrios = [900, 900, 1000, 80]
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgOpPrio :: Int
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendAltArgOpPrio = 80
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- Isabelle Terms representing the operations for CspProver
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | SKIP primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_skipOp = makeCspProverOpNoAlt cspProver_skipS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | STOP primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_stopOp = makeCspProverOpNoAlt cspProver_stopS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | DIV primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_divOp = makeCspProverOpNoAlt cspProver_divS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | RUN primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_runOp = makeCspProverOpNoAlt cspProver_runS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | CHAOS primitive process operator
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosOp :: Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_chaosOp = makeCspProverOpNoAlt cspProver_chaosS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Action prefix operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixOp :: Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_action_prefixOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeBinCspProverOp cspProver_action_prefixS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_action_prefixAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | External prefix choice operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceOp :: Term -> Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_external_prefix_choiceOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_external_prefix_choiceS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_external_prefix_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Internal prefix choice operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceOp :: Term -> Term -> Term -> Term
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_internal_prefix_choiceOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_internal_prefix_choiceS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_internal_prefix_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Sequence combinator operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_sequenceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_sequenceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_sequenceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_sequenceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | External choice operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_external_choiceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_external_choiceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_external_choiceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_external_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Internal choice operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_internal_choiceOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_internal_choiceOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_internal_choiceS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_internal_choiceAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Interleaving parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_interleavingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_interleavingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_interleavingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_interleavingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Synchronous parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_synchronousOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_synchronousOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_synchronousS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_synchronousAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Generalised parallel operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_general_parallelOp :: Term -> Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_general_parallelOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeTriCspProverOp cspProver_general_parallelS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_general_parallelAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Alphabetised parallel operator symbols
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_alphabetised_parallelOp :: Term -> Term -> Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_alphabetised_parallelOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeQuadCspProverOp cspProver_alphabetised_parallelS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltS
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltArgPrios
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly cspProver_alphabetised_parallelAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Hiding operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_hidingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_hidingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_hidingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_hidingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Renaming operator
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillycspProver_renamingOp :: Term -> Term -> Term
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycspProver_renamingOp =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly makeBinCspProverOp cspProver_renamingS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltS
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltArgPrios
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly cspProver_renamingAltOpPrio
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | Conditional operator
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillycspProver_conditionalOp :: Term -> Term -> Term -> Term
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_conditionalOp =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly makeTriCspProverOp cspProver_conditionalS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltS
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltArgPrios
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly cspProver_conditionalAltArgOpPrio
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Conditional operator
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycspProver_chan_nondeterministic_sendOp :: Term -> Term -> Term -> Term
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercspProver_chan_nondeterministic_sendOp =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly makeQuadCspProverOp cspProver_chan_nondeterministic_sendS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltArgPrios
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly cspProver_chan_nondeterministic_sendAltArgOpPrio
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a (Unary) CspProver operator
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederwith no alternative syntax -}
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian MaedermakeCspProverOpNoAlt :: String -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeCspProverOpNoAlt opName =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder con $ VName opName Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator with
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederalternative syntax -}
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeBinCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeBinCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in binVNameAppl vname t1 t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator (with 3
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparameters) with alternative syntax -}
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeTriCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeTriCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in termAppl (binVNameAppl vname t1 t2) t3
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Create an Isabelle Term representing a CspProver operator (with 4
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparameters) with alternative syntax -}
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeQuadCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly Term -> Term -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillymakeQuadCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 t4 =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly in termAppl (termAppl (binVNameAppl vname t1 t2) t3) t4