act ins10, optA, acc10, putA, coin, ready ; proc User = ins10 . optA . User ; Mach = acc10 . putA . Mach ; init allow( { coin, ready }, comm( { ins10|acc10 -> coin, optA|putA -> ready }, User || Mach ) ) ;