/* Tatica syncInput */
\tbegin
\ttactic syncInput()  \def

  \tappliesto\ ((\circvar\ dIn: \nat \circspot AIn \circseq AOut) \lpar ns_1 | \lchanset cs \rchanset  | ns_2 \rpar (\circvar\ dIn: \nat \circspot AIn \circseq ASt))
  
  \tdo (\tlaw VAR_EXP()
     \tsemi \tlaw Parallelism_composition_Sequence_Distribution2())


 \tend