BASIC-SPEC ::= BASIC-ITEMS...BASIC-ITEMS

| \{ \}

BASIC-ITEMS ::= channel/channels CHANNEL-ITEM ;...; CHANNEL-ITEM ;/

| process PROCESS-ITEM ;...; PROCESS-ITEM ;/

| ... %% other CASL basic items

CHANNEL-ITEM ::= CHANNEL ,..., CHANNEL : SORT

PROCESS-ITEM ::= PROCESS-NAME PROCESS-PROFILE %% declaration only

| PROCESS-NAME PROCESS-HEAD = PROCESS

| PROCESS-NAME = PROCESS

PROCESS-PROFILE ::= ( SORT ,..., SORT ) ALPHABET

| ALPHABET

PROCESS-HEAD ::= ( VAR ,..., VAR ) %% definition only

| ( ARG-DECL ;...; ARG-DECL) ALPHABET

| ALPHABET

EVENT-SET ::= SORT-OR-CHANNEL ,..., SORT-OR-CHANNEL

| \{ SORT-OR-CHANNEL ,..., SORT-OR-CHANNEL \}

| \{ \} %% empty set

ALPHABET ::= : EVENT-SET

| : %% empty alphabet

SORT-OR-CHANNEL ::= SORT

| CHANNEL

| CHANNEL : SORT

CHANNEL ::= SORT-ID

PROCESS-NAME ::= ID

PROCESS ::= ( PROCESS ) %% parenthesized process

| \"SKIP\"

| \"STOP\"

| \"DIV\"

| \"RUN\" ( EVENT-SET )

| \"CHAOS\" ( EVENT-SET )

| if FORMULA then PROCESS else PROCESS

| PROCESS-CALL

| PROCESS \back EVENT-SET %% hiding

| PROCESS [[ RENAMING ]]

| EVENT -> PROCESS

| TERM -> PROCESS

| [] VAR :: SORT -> PROCESS %% prefix choice

| |~| VAR :: SORT -> PROCESS

| PROCESS ; PROCESS

| PROCESS ;; PROCESS %% alternative syntax for sequential processes

| PROCESS [] PROCESS %% choice

| PROCESS |~| PROCESS

| PROCESS [| EVENT-SET |] PROCESS %% generalized

| PROCESS [ EVENT-SET || EVENT-SET ] PROCESS %% alphabetized

| PROCESS |[ EVENT-SET \| EVENT-SET ]| PROCESS %% alphabetized (alt.)

| PROCESS || PROCESS %% synchronous

| PROCESS ||| PROCESS %% interleaved

PROCESS-CALL ::= PROCESS-QUAL

| PROCESS-QUAL ( TERM ,..., TERM )

PROCESS-QUAL ::= PROCESS-NAME

| ( process PROCESS-NAME PROCESS-PROFILE )

RENAMING ::= ID ,..., ID %% unsupported

EVENT ::= CHANNEL ? VAR :: SORT

| CHANNEL ! VAR :: SORT

| CHANNEL ! TERM