# Machines calling machines ``` machine mA() { signal fa, fb, fc; state intial { } state other { copy fc; // fc' <= fc fa' --> hyper_transition; } state hyper_transition { var a; // constaints fa === fb + 1 if a == b { } fc', fd', v <== mB(fa, fb, v) --> other; } state other2 { fa , fb } state final { } } machine mB(signal in1, signal in2) (signal out1, signal out2) { singal fd, fe; state initial { } state middle { } state final { } } ``` ## SBPIR [{ + mB/initial + mB/middle + mB/final }, { + mA/initial + mA/other + mA/hyper_transition + mA/final }] ## SBPIR_multi steps: + mA/hyper_transition##mB/initial + mA/hyper_transition##mB/middle + mA/hyper_transition##mB/final [next step is mA/hyper_transition(post)] + mA/initial + mA/other + mA/hyper_transition(pre) [next step is mA/hyper_transition##mB/initial] + mA/hyper_transition(post) + mA/final trace: + mA/initial + mA/other + mA/hyper_transition(pre) + mB/initial + mB/middle + mB/final + mA/hyper_transition(post) + mA/final ## signals: currently: + forward + internal new type of signal, scoped: ScopedSignal(scope: Vec<String>, uuid) ScopedSingal(['mA/hyper_transition##mB']) ScopedSingal(['mA/hyper_transition##mB', 'initial']) Cell manager: signals without a common parent scope can share placement singals cannot share placement with a parent scope machine mX { signal a,b; state s1 { signal c, d; } state s2 { signal f; } } a -> (0,0), b -> (1, 0), c -> (0, 1), d -> (1, 1) f -> (0,1) In the new cell manager: SS([a]) :-: SS([b]) SS([a, d]) !:-: SS([a]) SS([a, d]) :-: SS([a, f]) C1 | C2 | C3 | C4 s1 a b c d s2 a b f a -> C1, b -> C2, c -> C3, f -> C3 match state { s1(a,b,c) s2(a,b,f) } [fa, fb, fc, fd, fe] mA/hyper_transition##mB ``` machine mA() { signal fa, fb, fc; state intial { } state other { } hyper_call hyper_transition { signal &a, &b, &c, &d; passthrough fa; &a, &b <== l + q, l &r <== fa &a, &b ==> mB ==> &c, &d // after the hyper transition reading fa t *s , s <== &c, &d } state hyper_transition ==> mB { } after { } state final { } } machine mB(signal in1, signal in2) (signal out1, signal out2) { singal fd, fe; state initial { } state middle { } state final { } } ```