Controller Synthesis for Deterministic Context Free Specification Languages
Sven Schneider, Anne-Kathrin Schmuck · DepositOnce · 2013
edge-pop=edge-pop e, edge-push=edge-push e, edge-trg=old (edge-trg e)|) definition FUNSR-else :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA1State, a, b)EDGE set where FUNSR-else e ≡ {FUNSR-E e} definition MixedReadEdge :: ( a, b, c)EDGE ⇒ bool where MixedReadEdge e ≡ edge-read e =None ∧ (edge-pop e =edge-push e) definition FUNSR :: ( q, a, b)EPDA ⇒ (( q, a, b) SDPDA1State, a, b)EPDA where FUNSR G ≡ (|epda-states=old ' (epda-states G) ∪ new ' (epda-delta G), epda-sigma=epda-sigma G, epda-gamma=epda-gamma G, epda-delta= (λe.if (MixedReadEdge e) then FUNSR-read e else FUNSR-else e)'(epda-delta G), epda-initial=old (epda-initial G), epda-box=epda-box G, epda-final=old ' (epda-final G)|) A.2.2 Remove No Operation definition FUNRNoOp-else :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA1State, a, b)EDGE where FUNRNoOp-else e ≡ (|edge-src=old (edge-src e), edge-read=edge-read e, edge-pop=edge-pop e, edge-push=edge-push e, edge-trg=old (edge-trg e)|) definition FUNRNoOp-ON :: ( q, a, b)EDGE ⇒ b ⇒ (( q, a, b) SDPDA1State, a, b)EDGE where FUNRNoOp-ON e PB ≡ (|edge-src=old (edge-src e), edge-read=None, edge-pop=edge-pop e, edge-push=[PB] @ (edge-pop e), edge-trg=new e|) definition FUNRNoOp-NO :: ( q, a, b)EDGE ⇒ b ⇒ (( q, a, b) SDPDA1State, a, b)EDGE where 64/113 FUNRNoOp-NO e PB ≡ (|edge-src=new e, edge-read=None, edge-pop=[PB], edge-push=[], edge-trg=old(edge-trg e)|) definition FUNRNoOp-NoOp :: ( q, a, b)EDGE ⇒ b ⇒ (( q, a, b) SDPDA1State, a, b)EDGE set where FUNRNoOp-NoOp e PB ≡ {FUNRNoOp-ON e PB,FUNRNoOp-NO e PB} definition FUNRNoOp :: ( q, a, b)EPDA ⇒ b ⇒ (( q, a, b) SDPDA1State, a, b)EPDA where FUNRNoOp G PB ≡ (|epda-states=old ' (epda-states G) ∪ new ' (epda-delta G), epda-sigma=epda-sigma G, epda-gamma=epda-gamma G ∪ {PB}, epda-delta= (λe.if NoOpEdge e then FUNRNoOp-NoOp e PB else {FUNRNoOp-else e})'(epda-delta G), epda-initial=old (epda-initial G), epda-box=epda-box G, epda-final=old ' (epda-final G)|) A.2.3 Split Push Pop definition FUNSPP-ON :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA1State, a, b)EDGE where FUNSPP-ON e ≡ (|edge-src=old (edge-src e), edge-read=None, edge-pop=edge-pop e, edge-push=[], edge-trg=new e|) definition FUNSPP-NO :: ( q, a, b)EDGE ⇒ b set ⇒ (( q, a, b) SDPDA1State, a, b)EDGE set where FUNSPP-NO e S ≡ { (|edge-src=new e, edge-read=None, edge-pop=[X], edge-push=edge-push e @ [X], edge-trg=old(edge-trg e)|)| X. X∈S} definition FUNSPP-NoOp :: ( q, a, b)EDGE ⇒ b set 65/113 ⇒ (( q, a, b) SDPDA1State, a, b)EDGE set where FUNSPP-NoOp e S ≡ {FUNSPP-ON e} ∪ FUNSPP-NO e S definition PushPopEdge :: ( q, a, b)EDGE ⇒ b ⇒ bool where PushPopEdge e BOX ≡ (edge-read e = None ∧ (∃ w b. edge-push e = w@[b] ∧ edge-pop e = [b])) definition FUNSPP-else :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA1State, a, b)EDGE where FUNSPP-else e ≡ (|edge-src=old (edge-src e), edge-read=edge-read e, edge-pop=edge-pop e, edge-push=edge-push e, edge-trg=old (edge-trg e)|) definition FUNSPP :: ( q, a, b)EPDA ⇒ (( q, a, b) SDPDA1State, a, b)EPDA where FUNSPP G ≡ (|epda-states=old ' (epda-states G) ∪ new ' (epda-delta G), epda-sigma=epda-sigma G, epda-gamma=epda-gamma G, epda-delta= (λe.if PushPopEdge e (epda-box G) then FUNSPP-NoOp e (epda-gamma G) else {FUNSPP-else e})'(epda-delta G), epda-initial=old (epda-initial G), epda-box=epda-box G, epda-final=old ' (epda-final G)|) A.2.4 Remove Multiple Push datatype ( q, a, b) SDPDA2State = old q | new ( q, a, b)EDGE nat definition FUNRMP-else :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA2State, a, b)EDGE where FUNRMP-else e ≡ (|edge-src=old (edge-src e), edge-read=edge-read e, edge-pop=edge-pop e, edge-push=edge-push e, edge-trg=old (edge-trg e)|) definition FUNRMP-state :: ( q, a, b)EDGE ⇒ nat ⇒ ( q, a, b) SDPDA2State option where FUNRMP-state e n ≡ 66/113 (if n=0 then Some (old (edge-src e)) else (if Suc n<length(edge-push e) then Some(new e n) else (if Suc n=length(edge-push e) then Some(old (edge-trg e)) else None))) definition FUNRMP-steps :: ( q, a, b)EDGE ⇒ (( q, a, b) SDPDA2State, a, b)EDGE set where FUNRMP-steps e ≡ (λi.{ (|edge-src=the(FUNRMP-state e i), edge-read=None, edge-pop=[(rev(edge-push e))!i], edge-push=[(rev(edge-push e))!(Suc i)]@[(rev(edge-push e))!i], edge-trg=the(FUNRMP-state e (Suc i))|) }) ' {i.0≤i ∧ Suc i