diff --git a/AlgebraicDataflowArchitectureModel/models/Algo.model b/AlgebraicDataflowArchitectureModel/models/Algo.model deleted file mode 100644 index 6228431..0000000 --- a/AlgebraicDataflowArchitectureModel/models/Algo.model +++ /dev/null @@ -1,12 +0,0 @@ -channel turnA{ - ref handsB(b:List, drawA(target:Int, guess:Int, b, d)) - ref deck(d:List, drawA(target, guess, b, d)) - out handsA(a:List, drawA(target, guess, b, d)) == if(eq(get(b, target), guess), cons(tuple(fst(head(d)), false), a), cons(tuple(fst(head(d)), true), a)) - out handsB(a:List, drawA(target, guess, b, d)) == if(eq(get(b, target), guess), set(a, target, tuple(fst(get(a, target)), true)), a) - out deck(t:List, drawA(target, guess, b, d)) == tail(d) -} -channel turnAA{ - ref handsB(b:List, selectA(target:Int, guess:Int, attacker:Int, b)) - out handsA(a:List, selectA(target, guess, attacker, b)) == if(eq(get(b, target), guess), a, set(a, attacker, tuple(fst(get(a, attacker)), true))) - out handsB(a:List, selectA(target, guess, attacker, b)) == if(eq(get(b, target), guess), set(a, target, tuple(fst(get(a, target)), true)), a) -} \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Algolike.model b/AlgebraicDataflowArchitectureModel/models/Algolike.model index 97aef04..3f6b5f7 100644 --- a/AlgebraicDataflowArchitectureModel/models/Algolike.model +++ b/AlgebraicDataflowArchitectureModel/models/Algolike.model @@ -6,25 +6,25 @@ guessB := 0 } channel targetAInput{ - out targetA(t:Int, setTargetA(a:Int)) == a + out targetA(t:Int, setTargetA(a:Int)) = a } channel targetBInput{ - out targetB(t:Int, setTargetB(b:Int)) == b + out targetB(t:Int, setTargetB(b:Int)) = b } channel attackerAInput{ - out attackerA(t:Int, setAttackerA(a:Int)) == a + out attackerA(t:Int, setAttackerA(a:Int)) = a } channel attackerBInput{ - out attackerB(t:Int, setAttackerB(b:Int)) == b + out attackerB(t:Int, setAttackerB(b:Int)) = b } channel guessAInput{ - out guessA(t:Int, setGuessA(a:Int)) == a + out guessA(t:Int, setGuessA(a:Int)) = a } channel guessBInput{ - out guessB(t:Int, setGuessB(b:Int)) == b + out guessB(t:Int, setGuessB(b:Int)) = b } channel addDeck{ - out deck(d:List, addCard(num:Integer)) == cons(tuple(num, false), d) + out deck(d:List, addCard(num:Integer)) = cons(tuple(num, false), d) } channel drawAInput{ @@ -32,21 +32,21 @@ ref targetA(t:Int, drawAndAttackA(t, g, b)) ref guessA(g:Int, drawAndAttackA(t, g, b)) ref handsB(b:List, drawAndAttackA(t, g, b)) - out resultByDrawingA(sda:Tuple, drawAndAttackA(t, g, b)) == tuple(eq(fst(get(b, t)), g), t) + out resultByDrawingA(sda:Tuple, drawAndAttackA(t, g, b)) = tuple(fst(get(b, t)) == g, t) } channel inputDrawArgsA{ - in resultByDrawingA(sda:Tuple, drawA(sucTrg, d)) == sucTrg + in resultByDrawingA(sda:Tuple, drawA(sucTrg, d)) = sucTrg ref deck(d:List, drawA(sucTrg, d)) - out handsA(outA:List, drawA(sucTrg, d)) == if(fst(sucTrg), - sortByKey(cons(tuple(fst(head(d)),false), outA)), + out handsA(outA:List, drawA(sucTrg, d)) = if(fst(sucTrg), + sortByKey(cons(tuple(fst(head(d)), false), outA)), sortByKey(cons(tuple(fst(head(d)), true), outA))) - out handsB(outB:List, drawA(sucTrg, d)) == if(fst(sucTrg), + out handsB(outB:List, drawA(sucTrg, d)) = if(fst(sucTrg), set(outB, snd(sucTrg), tuple(fst(get(outB, snd(sucTrg))), true)), outB) - out deck(t:List, drawA(sucTrg, d)) == tail(t) + out deck(t:List, drawA(sucTrg, d)) = tail(t) } channel selectAInput{ @@ -54,14 +54,14 @@ ref targetA(t:Int, selectAndAttackA(a, t, g, b)) ref guessA(g:Int, selectAndAttackA(a, t, g, b)) ref handsB(b:List, selectAndAttackA(a, t, g, b)) - out resultBySelectingA(ssa:Tuple, selectAndAttackA(a, t, g, b)) == tuple(eq(fst(get(b, t)), g), t, a) + out resultBySelectingA(ssa:Tuple, selectAndAttackA(a, t, g, b)) = tuple(fst(get(b, t)) == g, t, a) } channel inputSelectArgA{ - in resultBySelectingA(ssa, selectA(sucTrgAtk)) == sucTrgAtk - out handsA(outA, selectA(sucTrgAtk)) == if(fst(sucTrgAtk), + in resultBySelectingA(ssa, selectA(sucTrgAtk)) = sucTrgAtk + out handsA(outA, selectA(sucTrgAtk)) = if(fst(sucTrgAtk), outA, set(outA, snd(snd(sucTrgAtk)), tuple(fst(get(outA, snd(snd(sucTrgAtk)))), true))) - out handsB(outB, selectA(sucTrgAtk)) == if(fst(sucTrgAtk), + out handsB(outB, selectA(sucTrgAtk)) = if(fst(sucTrgAtk), set(outB, fst(snd(sucTrgAtk)), tuple(fst(get(outB, fst(snd(sucTrgAtk)))), true)), outB) } @@ -69,21 +69,21 @@ ref targetB(t:Int, drawAndAttackB(t, g, a)) ref guessB(g:Int, drawAndAttackB(t, g, a)) ref handsA(a:List, drawAndAttackB(t, g, a)) - out resultByDrawingB(sdb:Tuple, drawAndAttackB(t, g, a)) == tuple(eq(fst(get(a, t)), g), t) + out resultByDrawingB(sdb:Tuple, drawAndAttackB(t, g, a)) = tuple(fst(get(a, t)) == g, t) } channel inputDrawArgsB{ - in resultByDrawingB(sdb:Tuple, drawB(sucTrg, d)) == sucTrg + in resultByDrawingB(sdb:Tuple, drawB(sucTrg, d)) = sucTrg ref deck(d:List, drawB(sucTrg, d)) - out handsB(outB:List, drawB(sucTrg, d)) == if(fst(sucTrg), + out handsB(outB:List, drawB(sucTrg, d)) = if(fst(sucTrg), sortByKey(cons(tuple(fst(head(d)),false), outB)), sortByKey(cons(tuple(fst(head(d)), true), outB))) - out handsA(outA:List, drawB(sucTrg, d)) == if(fst(sucTrg), + out handsA(outA:List, drawB(sucTrg, d)) = if(fst(sucTrg), set(outA, snd(sucTrg), tuple(fst(get(outA, snd(sucTrg))), true)), outA) - out deck(t:List, drawB(sucTrg, d)) == tail(t) + out deck(t:List, drawB(sucTrg, d)) = tail(t) } channel selectBInput{ @@ -91,23 +91,23 @@ ref targetB(t:Int, selectAndAttackB(atk, t, g, a)) ref guessB(g:Int, selectAndAttackB(atk, t, g, a)) ref handsA(a:List, selectAndAttackB(atk, t, g, a)) - out resultBySelectingB(ssb:Tuple, selectAndAttackB(atk, t, g, a)) == tuple(eq(fst(get(a, t)), g), t, atk) + out resultBySelectingB(ssb:Tuple, selectAndAttackB(atk, t, g, a)) = tuple(fst(get(a, t)) == g, t, atk) } channel inputSelectArgB{ - in resultBySelectingB(ssb, selectB(sucTrgAtk)) == sucTrgAtk - out handsB(outB, selectB(sucTrgAtk)) == if(fst(sucTrgAtk), + in resultBySelectingB(ssb, selectB(sucTrgAtk)) = sucTrgAtk + out handsB(outB, selectB(sucTrgAtk)) = if(fst(sucTrgAtk), outB, set(outB, snd(snd(sucTrgAtk)), tuple(fst(get(outB, snd(snd(sucTrgAtk)))), true))) - out handsA(outA, selectB(sucTrgAtk)) == if(fst(sucTrgAtk), + out handsA(outA, selectB(sucTrgAtk)) = if(fst(sucTrgAtk), set(outA, fst(snd(sucTrgAtk)), tuple(fst(get(outA, fst(snd(sucTrgAtk)))), true)), outA) } channel judgeA{ - in handsA(a:List, judge(j)) == j - out loseA(la:Bool, judge(j)) == eq(length(extractFaceDown(j)), 0) + in handsA(a:List, judge(j)) = j + out loseA(la:Bool, judge(j)) = (length(extractFaceDown(j)) == 0) } channel judgeB{ - in handsB(b:List, judge(j)) == j - out loseB(lb:Bool, judge(j)) == eq(length(extractFaceDown(j)), 0) + in handsB(b:List, judge(j)) = j + out loseB(lb:Bool, judge(j)) = (length(extractFaceDown(j)) == 0) } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Base.model b/AlgebraicDataflowArchitectureModel/models/Base.model index ac44843..bb460e4 100644 --- a/AlgebraicDataflowArchitectureModel/models/Base.model +++ b/AlgebraicDataflowArchitectureModel/models/Base.model @@ -1,13 +1,13 @@ channel CIO{ - out r1(x1:Int, set1(y1:Int)) == y1 - out r1(x1, e) == x1 + out r1(x1:Int, set1(y1:Int)) = y1 + out r1(x1, e) = x1 } channel CIO2{ - out r2(x2:Int, set2(y2:Int)) == y2 - out r2(x2, e) == x2 + out r2(x2:Int, set2(y2:Int)) = y2 + out r2(x2, e) = x2 } channel C1{ - in r1(x1, update(x1:Int, y1:Int, x2:Int, y2:Int)) == y1 - in r2(x2, update(x1, y1, x2, y2)) == y2 - out r3(x3:Int, update(x1, y1, x2, y2)) == x1 + y1 + x2 + y2 + in r1(x1, update(x1:Int, y1:Int, x2:Int, y2:Int)) = y1 + in r2(x2, update(x1, y1, x2, y2)) = y2 + out r3(x3:Int, update(x1, y1, x2, y2)) = x1 + y1 + x2 + y2 } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Bug.model b/AlgebraicDataflowArchitectureModel/models/Bug.model deleted file mode 100644 index f31727b..0000000 --- a/AlgebraicDataflowArchitectureModel/models/Bug.model +++ /dev/null @@ -1,7 +0,0 @@ -channel CIO{ - out aUa(a, input(x:Int)) == x -} -channel C1{ - in aUa(a, update(x)) == x - out aUb(b, update(x)) == x + 3 -} \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Clock.dtram b/AlgebraicDataflowArchitectureModel/models/Clock.dtram new file mode 100644 index 0000000..ec23d75 --- /dev/null +++ b/AlgebraicDataflowArchitectureModel/models/Clock.dtram @@ -0,0 +1,27 @@ +model { + channel CIO1 { + out min(m: Int, tick) = (m + 1) % 60 + } + channel Clock { + in min(m, update(m2)) = m2 + out hour(h: Int, update(m2)) = if(m2 == 0, (h + 1) % 24, h) + } + channel MinUpdate { + in min(m, update(m2)) = m2 + out min_ang(m_ang: Double, update(m2)) = m2 / 30 * PI + } + channel HourUpdate { + in hour(h, update(h2)) = h2 + out hour_ang(h_ang: Double, update(h2)) = h2 / 6 * PI + } +} +geometry { + node c HourUpdate:520,340,30,30 + node c MinUpdate:520,100,30,30 + node c Clock:280,220,30,30 + node r min_ang:670,100,80,30 + node r min:250,100,80,30 + node r hour:270,340,80,30 + node r hour_ang:680,340,80,30 + node ioc CIO1:100,100,30,30 +} diff --git a/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model b/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model index f140bff..dced55e 100644 --- a/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model +++ b/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model @@ -1,33 +1,33 @@ channel C_CustomerAOff_In { - out customerA_off(c:String, setOff(x)) == x - out customerA_off(c, e) == c + out customerA_off(c:String, setOff(x)) = x + out customerA_off(c, e) = c } channel C_CustomerBOff_In { - out customerB_off(c:String, setOff(x)) == x - out customerB_off(c, e) == c + out customerB_off(c:String, setOff(x)) = x + out customerB_off(c, e) = c } channel C_CompanyC1Add_In { - out companyC1_add(a:String, setAdd(y)) == y - out companyC1_add(a, e) == a + out companyC1_add(a:String, setAdd(y)) = y + out companyC1_add(a, e) = a } channel C_CompanyC2Add_In { - out companyC2_add(a:String, setAdd(y)) == y - out companyC2_add(a, e) == a + out companyC2_add(a:String, setAdd(y)) = y + out companyC2_add(a, e) = a } channel CA { - in customerA_off(c, sync(z, u, v)) == z - in companyC1_add(a1, sync(z, u, v)) == u - in companyC2_add(a2, sync(z, u, v)) == v - out customerA_add(a3:String, sync(z, u, v)) == if(eq(z, C1), u, if(eq(z, C2), v, null)) + in customerA_off(c, sync(z, u, v)) = z + in companyC1_add(a1, sync(z, u, v)) = u + in companyC2_add(a2, sync(z, u, v)) = v + out customerA_add(a3:String, sync(z, u, v)) = if(z == C1, u, if(z == C2, v, null)) } channel CB { - in customerB_off(c, sync(z, u, v)) == z - in companyC1_add(a1, sync(z, u, v)) == u - in companyC2_add(a2, sync(z, u, v)) == v - out customerB_add(a3:String, sync(z, u, v)) == if(eq(z, C1), u, if(eq(z, C2), v, null)) + in customerB_off(c, sync(z, u, v)) = z + in companyC1_add(a1, sync(z, u, v)) = u + in companyC2_add(a2, sync(z, u, v)) = v + out customerB_add(a3:String, sync(z, u, v)) = if(z == C1, u, if(z == C2, v, null)) } diff --git a/AlgebraicDataflowArchitectureModel/models/Game.model b/AlgebraicDataflowArchitectureModel/models/Game.model index bc90ba4..1952ff0 100644 --- a/AlgebraicDataflowArchitectureModel/models/Game.model +++ b/AlgebraicDataflowArchitectureModel/models/Game.model @@ -1,32 +1,32 @@ channel CIO { - out force(f:Double, action(x:Double)) == x - out time(t:Double, action(x)) == t + 0.01 - out force(f, e) == x - out time(t, e) == t + 0.01 + out force(f:Double, action(x:Double)) = x + out time(t:Double, action(x)) = t + 0.01 + out force(f, e) = x + out time(t, e) = t + 0.01 } channel CIO2 { - out velocity(v:Double, setVel(x:Double)) == x - out velocity(v, e) == x + out velocity(v:Double, setVel(x:Double)) = x + out velocity(v, e) = x } channel CIO3 { - out mass(m:Double, setMass(x:Double)) == x - out mass(m, e) == m + out mass(m:Double, setMass(x:Double)) = x + out mass(m, e) = m } channel C1 { - in force(f, update1(y, z)) == y - in mass(m, update1(y, z)) == z - out acceleration(a: Double, update1(y, z)) == y / z + in force(f, update1(y, z)) = y + in mass(m, update1(y, z)) = z + out acceleration(a: Double, update1(y, z)) = y / z } channel C2 { - in acceleration(a, update2(z)) == z - out velocity(v:Double, update2(z)) == v + 0.01 * z + in acceleration(a, update2(z)) = z + out velocity(v:Double, update2(z)) = v + 0.01 * z } channel C3 { - in velocity(v, update3(u)) == u - out position(p:Double, update3(u)) == p + 0.01 * u + in velocity(v, update3(u)) = u + out position(p:Double, update3(u)) = p + 0.01 * u } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Hello.model b/AlgebraicDataflowArchitectureModel/models/Hello.model deleted file mode 100644 index 46bb932..0000000 --- a/AlgebraicDataflowArchitectureModel/models/Hello.model +++ /dev/null @@ -1,3 +0,0 @@ -channel cio { - out r1(x1:Int,set(x2)) == x2 -} diff --git a/AlgebraicDataflowArchitectureModel/models/Hello2.model b/AlgebraicDataflowArchitectureModel/models/Hello2.model deleted file mode 100644 index 4815cf6..0000000 --- a/AlgebraicDataflowArchitectureModel/models/Hello2.model +++ /dev/null @@ -1,3 +0,0 @@ -channel cio { - out r1(x1:Int,set(x2:Int)) == x2:Int -} diff --git a/AlgebraicDataflowArchitectureModel/models/HelloWorld.model b/AlgebraicDataflowArchitectureModel/models/HelloWorld.model deleted file mode 100644 index 44aa310..0000000 --- a/AlgebraicDataflowArchitectureModel/models/HelloWorld.model +++ /dev/null @@ -1,7 +0,0 @@ -channel cio { - out r1(x1:Int,set(x2:Int)) == x2:Int -} -channel c2 { - in r1(x1:Int,update(x2:Int)) == x2:Int - out r2(y1:Int,update(x2:Int)) == (x2:Int+1) -} diff --git a/AlgebraicDataflowArchitectureModel/models/JumpGame.model b/AlgebraicDataflowArchitectureModel/models/JumpGame.model index 1981df9..43b8d0c 100644 --- a/AlgebraicDataflowArchitectureModel/models/JumpGame.model +++ b/AlgebraicDataflowArchitectureModel/models/JumpGame.model @@ -1,7 +1,8 @@ init { force := pair(0.0, 0.0) time := 0.0 - move := pair(0.0, 0.0) + movex := 0.0 + movey := 0.0 mass := 1.0 ground := true acceleration := pair(0.0, 0.0) @@ -12,59 +13,59 @@ gameover := false } channel CIO { - out force(f:Pair, gravity(y:Double)) == pair(0.0, y) - out time(t:Double, gravity(y)) == t + 0.01 + out force(f:Pair, gravity(y:Double)) = pair(0.0, y) + out time(t:Double, gravity(y)) = t + 0.01 } channel CIO2 { - out movex(x:Double, run(x2:Double)) == x2 + out movex(x:Double, run(x2:Double)) = x2 } channel CIO3 { - out movey(y:Double, jump(y2:Double)) == y2 + out movey(y:Double, jump(y2:Double)) = y2 } channel CIO4 { - out mass(m:Double, setMass(x:Double)) == x + out mass(m:Double, setMass(x:Double)) = x } channel CIO5 { - out ground(g:Bool, openHole) == false - out ground(g, closeHole) == true + out ground(g:Bool, openHole) = false + out ground(g, closeHole) = true } channel C1 { ref onground(o, update1(f2, m2, o)) - in force(f, update1(f2, m2, o)) == f2 - in mass(m, update1(f2, m2, o)) == m2 - out acceleration(a:Pair, update1(f2, m2, o)) == if(o, pair(left(f2) / m2, 0.0), pair(left(f2) / m2, right(f2) / m2)) + in force(f, update1(f2, m2, o)) = f2 + in mass(m, update1(f2, m2, o)) = m2 + out acceleration(a:Pair, update1(f2, m2, o)) = if(o, pair(left(f2) / m2, 0.0), pair(left(f2) / m2, right(f2) / m2)) } channel C2 { ref onground(o, update3(a2, o)) - in acceleration(a, update3(a2, o)) == a2 - out velocity(v:Pair, update3(a2, o)) == if(and(o, lt(right(v), 0.0)), + in acceleration(a, update3(a2, o)) = a2 + out velocity(v:Pair, update3(a2, o)) = if(o && right(v) < 0.0, pair(left(v) + 0.01 * left(a2), 0.0), pair(left(v) + 0.01 * left(a2), right(v) + 0.01 * right(a2))) } channel C3 { ref onground(o, update4(x2, o)) - in movex(x, update4(x2, o)) == x2 - out velocity(v:Pair, update4(x2, o)) == if(o, pair(x2, right(v)), v) + in movex(x, update4(x2, o)) = x2 + out velocity(v:Pair, update4(x2, o)) = if(o, pair(x2, right(v)), v) } channel C4 { ref onground(o, update5(x2, o)) - in movey(y, update5(y2, o)) == y2 - out velocity(v:Pair, update5(y2, o)) == if(o, pair(left(v), y2), v) + in movey(y, update5(y2, o)) = y2 + out velocity(v:Pair, update5(y2, o)) = if(o, pair(left(v), y2), v) } channel C5 { - in velocity(v, update6(v2, g)) == v2 + in velocity(v, update6(v2, g)) = v2 ref ground(g, update6(v2, g)) - out position(p:Pair, update6(v2, g)) == if(and(eq(g, true), lt(right(p) + 0.01 * right(v2), 0.0)), + out position(p:Pair, update6(v2, g)) = if(g == true && right(p) + 0.01 * right(v2) > 0.0, pair(left(p) + 0.01 * left(v2), 0.0), pair(left(p) + 0.01 * left(v2), right(p) + 0.01 * right(v2))) } channel C6 { - in position(p, update2(p2, g2)) == p2 - in ground(g, update2(p2, g2)) == g2 - out onground(o:Bool, update2(p2, g2)) == and(eq(g2, true), le(right(p2), 0.0)) + in position(p, update2(p2, g2)) = p2 + in ground(g, update2(p2, g2)) = g2 + out onground(o:Bool, update2(p2, g2)) = (g2 == true && right(p2) <= 0.0) } channel C7 { - in position(p, update7(p2)) == p2 - out clear(c:Bool, update7(p2)) == if(gt(left(p2), 100.0), true, false) - out gameover(go:Bool, update7(p2)) == if(lt(right(p2), -1.0), true, false) + in position(p, update7(p2)) = p2 + out clear(c:Bool, update7(p2)) = (left(p2) > 100.0) + out gameover(go:Bool, update7(p2)) = (right(p2) < -1.0) } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Kinetics.model b/AlgebraicDataflowArchitectureModel/models/Kinetics.model index 5218206..3d10af4 100644 --- a/AlgebraicDataflowArchitectureModel/models/Kinetics.model +++ b/AlgebraicDataflowArchitectureModel/models/Kinetics.model @@ -1,20 +1,20 @@ channel CIO { - out force(f:Double, action(x)) == x - out time(t:Double, action(x)) == t + 0.01 + out force(f:Double, action(x)) = x + out time(t:Double, action(x)) = t + 0.01 } channel C1 { - in force(f, update1(y, m)) == y - in mass(m, update1(y, m)) == m - out acceleration(a:Double, update1(y, m)) == y / m + in force(f, update1(y, m)) = y + in mass(m, update1(y, m)) = m + out acceleration(a:Double, update1(y, m)) = y / m } channel C2 { - in acceleration(a, update2(z)) == z - out velocity(v:Double, update2(z)) == v + 0.01 * z + in acceleration(a, update2(z)) = z + out velocity(v:Double, update2(z)) = v + 0.01 * z } channel C3 { - in velocity(v, update3(u)) == u - out position(p:Double, update3(u)) == p + 0.01 * u + in velocity(v, update3(u)) = u + out position(p:Double, update3(u)) = p + 0.01 * u } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/POS.dtram b/AlgebraicDataflowArchitectureModel/models/POS.dtram index dc3d2d1..d1cb11c 100644 --- a/AlgebraicDataflowArchitectureModel/models/POS.dtram +++ b/AlgebraicDataflowArchitectureModel/models/POS.dtram @@ -1,18 +1,18 @@ model { channel CIO { - out payment(p:Int, purchase(x:Int)) == x + out payment(p:Int, purchase(x:Int)) = x } channel C3 { - in history(h, update3(u)) == u - out total(t:Int, update3(u)) == sum(u) + in history(h, update3(u)) = u + out total(t:Int, update3(u)) = sum(u) } channel C1 { - in payment(p, update1(y)) == y - out points(l:Int, update1(y)) == floor(y * 0.05) + in payment(p, update1(y)) = y + out points(l:Int, update1(y)) = floor(y * 0.05) } channel C2 { - in payment(p, update2(z)) == z - out history(h:List, update2(z)) == cons(z, h) + in payment(p, update2(z)) = z + out history(h:List, update2(z)) = cons(z, h) } } geometry { diff --git a/AlgebraicDataflowArchitectureModel/models/POS.model b/AlgebraicDataflowArchitectureModel/models/POS.model index 150c106..c15c931 100644 --- a/AlgebraicDataflowArchitectureModel/models/POS.model +++ b/AlgebraicDataflowArchitectureModel/models/POS.model @@ -1,15 +1,15 @@ channel CIO { - out payment(p:Int, purchase(x:Int)) == x + out payment(p:Int, purchase(x:Int)) = x } channel C3 { - in history(h, update3(u)) == u - out total(t:Int, update3(u)) == sum(u) + in history(h, update3(u)) = u + out total(t:Int, update3(u)) = sum(u) } channel C1 { - in payment(p, update1(y)) == y - out points(l:Int, update1(y)) == floor(y * 0.05) + in payment(p, update1(y)) = y + out points(l:Int, update1(y)) = floor(y * 0.05) } channel C2 { - in payment(p, update2(z)) == z - out history(h:List, update2(z)) == cons(z, h) + in payment(p, update2(z)) = z + out history(h:List, update2(z)) = cons(z, h) } diff --git a/AlgebraicDataflowArchitectureModel/models/POS2.model b/AlgebraicDataflowArchitectureModel/models/POS2.model index 6ae676d..0ee31d2 100644 --- a/AlgebraicDataflowArchitectureModel/models/POS2.model +++ b/AlgebraicDataflowArchitectureModel/models/POS2.model @@ -1,14 +1,14 @@ channel CIO { - out payment(p:Int, purchase(x:Int)) == x + out payment(p:Int, purchase(x:Int)) = x } channel C1 { - in payment(p1, update1(y)) == y - out points(l:Int, update1(y)) == floor(y * 0.05) + in payment(p1, update1(y)) = y + out points(l:Int, update1(y)) = floor(y * 0.05) } channel C2 { - in payment(p1, update2(z)) == z - out history(h:List, update2(z)) == cons(z, h) - out total(t:Int, update2(z)) == z + t + in payment(p1, update2(z)) = z + out history(h:List, update2(z)) = cons(z, h) + out total(t:Int, update2(z)) = z + t } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/StockManagement.model b/AlgebraicDataflowArchitectureModel/models/StockManagement.model index b133f44..4528cb7 100644 --- a/AlgebraicDataflowArchitectureModel/models/StockManagement.model +++ b/AlgebraicDataflowArchitectureModel/models/StockManagement.model @@ -4,47 +4,47 @@ } channel CIO_enter { - out arrival(s:Tuple, arrive(item:Str, num:Int)) == tuple(item, num) + out arrival(s:Tuple, arrive(item:Str, num:Int)) = tuple(item, num) } channel CIO_req { - out request(r:Tuple, req(item:Str, num:Int)) == tuple(item, num) + out request(r:Tuple, req(item:Str, num:Int)) = tuple(item, num) } channel C1 { - in arrival(ar, update1(ar2, st)) == ar2 + in arrival(ar, update1(ar2, st)) = ar2 ref stock(st:Map, update1(ar2, st)) - out available(av:Tuple, update1(ar2, st)) == tuple(fst(ar2), snd(ar2) + lookup(st, fst(ar2))) + out available(av:Tuple, update1(ar2, st)) = tuple(fst(ar2), snd(ar2) + lookup(st, fst(ar2))) } channel C2 { - in available(av, update2(av2, sh)) == av2 + in available(av, update2(av2, sh)) = av2 ref shortage(sh, update2(av2, sh)) - out deriver(dr:Tuple, update2(av2, sh)) == if(ge(snd(av2), lookup(sh, fst(av2))), + out deriver(dr:Tuple, update2(av2, sh)) = if(snd(av2) >= lookup(sh, fst(av2)), tuple(fst(av2), lookup(sh, fst(av2)), snd(av2) - lookup(sh, fst(av2))), tuple(fst(av2), 0, snd(av2))) - out shortage(s, update2(av2, sh)) == if(ge(snd(av2), lookup(s, fst(av2))), + out shortage(s, update2(av2, sh)) = if(snd(av2) >= lookup(s, fst(av2)), insert(s, fst(av2), 0), s) } channel C3 { - in deriver(dr, update3(dr2)) == dr2 - out stock(st, update3(dr2)) == insert(st, fst(dr2), snd(snd(dr2))) + in deriver(dr, update3(dr2)) = dr2 + out stock(st, update3(dr2)) = insert(st, fst(dr2), snd(snd(dr2))) } channel C4 { - in deriver(dr, update4(dr2)) == dr2 - out shipping(sp:Tuple, update4(dr2)) == tuple(fst(dr2), fst(snd(dr2))) + in deriver(dr, update4(dr2)) = dr2 + out shipping(sp:Tuple, update4(dr2)) = tuple(fst(dr2), fst(snd(dr2))) } channel C5 { - in request(rq, update5(rq2, st)) == rq2 + in request(rq, update5(rq2, st)) = rq2 ref stock(st, update5(rq2, st)) - out deriver(dr, update5(rq2, st)) == if(ge(lookup(st, fst(rq2)), snd(rq2)), + out deriver(dr, update5(rq2, st)) = if(lookup(st, fst(rq2)) >= snd(rq2), tuple(fst(rq2), snd(rq2), lookup(st, fst(rq2)) - snd(rq2)), tuple(fst(rq2), 0, lookup(st, fst(rq2)))) - out shortage(sh, update5(rq2, st)) == if(ge(lookup(st, fst(rq2)), snd(rq2)), + out shortage(sh, update5(rq2, st)) = if(lookup(st, fst(rq2)) >= snd(rq2), sh, insert(sh, fst(rq2), lookup(sh, fst(rq2)) + snd(rq2))) } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/StockManagement2.model b/AlgebraicDataflowArchitectureModel/models/StockManagement2.model deleted file mode 100644 index 6ee866a..0000000 --- a/AlgebraicDataflowArchitectureModel/models/StockManagement2.model +++ /dev/null @@ -1,13 +0,0 @@ -init { - stock := nil - shortage := nil -} - -channel CIO_enter { - out deriver(s:Tuple, arrive(item:Str, num:Int)) == tuple(item, num, num) -} - -channel C3 { - in deriver(dr, update3(dr2)) == dr2 - out shipping(sp:Tuple, update3(dr2)) == tuple(fst(dr2), fst(snd(dr2))) -} diff --git a/AlgebraicDataflowArchitectureModel/models/Test.model b/AlgebraicDataflowArchitectureModel/models/Test.model deleted file mode 100644 index a8a1348..0000000 --- a/AlgebraicDataflowArchitectureModel/models/Test.model +++ /dev/null @@ -1,9 +0,0 @@ -channel CIO { - out a(x:Int, set(n:Int)) == n -} - -channel C1 { - in a(x, update(y)) == y - out b(z, update(y)) == y + 1 - out c(v, update(y)) == v + y -} \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/TravelDistance.model b/AlgebraicDataflowArchitectureModel/models/TravelDistance.model index a0c8fe2..07d12db 100644 --- a/AlgebraicDataflowArchitectureModel/models/TravelDistance.model +++ b/AlgebraicDataflowArchitectureModel/models/TravelDistance.model @@ -1,13 +1,13 @@ channel CX { - out pos_x(prev_x: Double, setX(cur_x: Double)) == cur_x + out pos_x(prev_x: Double, setX(cur_x: Double)) = cur_x } channel CY { - out pos_y(prev_y: Double, setY(cur_y: Double)) == cur_y + out pos_y(prev_y: Double, setY(cur_y: Double)) = cur_y } channel C { - in pos_x(prev_x, move(dx, dy)) == prev_x + dx - in pos_y(prev_y, move(dx, dy)) == prev_y + dy - out dist(prev_d, move(dx, dy)) == prev_d + sqrt(dx * dx + dy * dy) + in pos_x(prev_x, move(dx, dy)) = prev_x + dx + in pos_y(prev_y, move(dx, dy)) = prev_y + dy + out dist(prev_d, move(dx, dy)) = prev_d + sqrt(dx * dx + dy * dy) } diff --git a/AlgebraicDataflowArchitectureModel/models/Triangle.model b/AlgebraicDataflowArchitectureModel/models/Triangle.model new file mode 100644 index 0000000..cf3d0e0 --- /dev/null +++ b/AlgebraicDataflowArchitectureModel/models/Triangle.model @@ -0,0 +1,13 @@ +channel cio1 { + out base(x: Double, setBase(x2)) = x2 +} + +channel cio2 { + out height(y: Double, setHeight(y2)) = y2 +} + +channel triangle { + in base(x, update(x2, y2)) = x2 + in height(y, update(x2, y2)) = y2 + out hypothenuse(z: Double, update(x2, y2)) = sqrt(x2 * x2 + y2 * y2) +} \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Triangle2.model b/AlgebraicDataflowArchitectureModel/models/Triangle2.model new file mode 100644 index 0000000..5067fa0 --- /dev/null +++ b/AlgebraicDataflowArchitectureModel/models/Triangle2.model @@ -0,0 +1,13 @@ +channel cio1 { + out base(x: Double, setBase(x2)) = x2 +} + +channel cio2 { + out height(y: Double, setHeight(y2)) = y2 +} + +channel triangle { + in base(x, update: Tuple) = fst(update) + in height(y, update) = snd(update) + out hypothenuse(z: Double, update) = sqrt(fst(update) * fst(update) + snd(update) * snd(update)) +} \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Twitter.model b/AlgebraicDataflowArchitectureModel/models/Twitter.model index 57de3b3..b5c0ee5 100644 --- a/AlgebraicDataflowArchitectureModel/models/Twitter.model +++ b/AlgebraicDataflowArchitectureModel/models/Twitter.model @@ -1,47 +1,47 @@ channel a_Tweet { - out a_tweets(l:List, a_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) + out a_tweets(l:List, a_tweet(t:Str, time:Long)) = cons(tuple(time, t), l) } channel a_Follow { - out a_following(f:List, a_follow(u:Int)) == cons(u, f) + out a_following(f:List, a_follow(u:Int)) = cons(u, f) } channel a_Home { - in a_tweets(la1, update_a(f2, la2, lb2, lc2)) == la2 - in b_tweets(lb1, update_a(f2, la2, lb2, lc2)) == lb2 - in c_tweets(lc1, update_a(f2, la2, lb2, lc2)) == lc2 - in a_following(f, update_a(f2, la2, lb2, lc2)) == f2 - out a_timeline(t:List, update_a(f2, la2, lb2, lc2)) == merge(la2, if(contains(f2,2), merge(lb2, if(contains(f2,3), lc2, nil)), if(contains(f2,3), lc2, nil))) + in a_tweets(la1, update_a(f2, la2, lb2, lc2)) = la2 + in b_tweets(lb1, update_a(f2, la2, lb2, lc2)) = lb2 + in c_tweets(lc1, update_a(f2, la2, lb2, lc2)) = lc2 + in a_following(f, update_a(f2, la2, lb2, lc2)) = f2 + out a_timeline(t:List, update_a(f2, la2, lb2, lc2)) = merge(la2, if(contains(f2,2), merge(lb2, if(contains(f2,3), lc2, nil)), if(contains(f2,3), lc2, nil))) } channel b_Tweet { - out b_tweets(l:List, b_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) + out b_tweets(l:List, b_tweet(t:Str, time:Long)) = cons(tuple(time, t), l) } channel b_Follow { - out b_following(f:List, b_follow(u:Int)) == cons(u, f) + out b_following(f:List, b_follow(u:Int)) = cons(u, f) } channel b_Home { - in a_tweets(la1, update_b(f2, la2, lb2, lc2)) == la2 - in b_tweets(lb1, update_b(f2, la2, lb2, lc2)) == lb2 - in c_tweets(lc1, update_b(f2, la2, lb2, lc2)) == lc2 - in b_following(f, update_b(f2, la2, lb2, lc2)) == f2 - out b_timeline(t:List, update_b(f2, la2, lb2, lc2)) == merge(lb2, if(contains(f2,1), merge(la2, if(contains(f2,3), lc2, nil)), if(contains(f2,3), lc2, nil))) + in a_tweets(la1, update_b(f2, la2, lb2, lc2)) = la2 + in b_tweets(lb1, update_b(f2, la2, lb2, lc2)) = lb2 + in c_tweets(lc1, update_b(f2, la2, lb2, lc2)) = lc2 + in b_following(f, update_b(f2, la2, lb2, lc2)) = f2 + out b_timeline(t:List, update_b(f2, la2, lb2, lc2)) = merge(lb2, if(contains(f2,1), merge(la2, if(contains(f2,3), lc2, nil)), if(contains(f2,3), lc2, nil))) } channel c_Tweet { - out c_tweets(l:List, c_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) + out c_tweets(l:List, c_tweet(t:Str, time:Long)) = cons(tuple(time, t), l) } channel c_Follow { - out c_following(f:List, c_follow(u:Int)) == cons(u, f) + out c_following(f:List, c_follow(u:Int)) = cons(u, f) } channel c_Home { - in a_tweets(la1, update_c(f2, la2, lb2, lc2)) == la2 - in b_tweets(lb1, update_c(f2, la2, lb2, lc2)) == lb2 - in c_tweets(lc1, update_c(f2, la2, lb2, lc2)) == lc2 - in c_following(f, update_c(f2, la2, lb2, lc2)) == f2 - out c_timeline(t:List, update_c(f2, la2, lb2, lc2)) == merge(lc2, if(contains(f2,1), merge(la2, if(contains(f2,2), lb2, nil)), if(contains(f2,2), lb2, nil))) + in a_tweets(la1, update_c(f2, la2, lb2, lc2)) = la2 + in b_tweets(lb1, update_c(f2, la2, lb2, lc2)) = lb2 + in c_tweets(lc1, update_c(f2, la2, lb2, lc2)) = lc2 + in c_following(f, update_c(f2, la2, lb2, lc2)) = f2 + out c_timeline(t:List, update_c(f2, la2, lb2, lc2)) = merge(lc2, if(contains(f2,1), merge(la2, if(contains(f2,2), lb2, nil)), if(contains(f2,2), lb2, nil))) } diff --git a/AlgebraicDataflowArchitectureModel/models/WOS.dtram b/AlgebraicDataflowArchitectureModel/models/WOS.dtram index 45f640c..81b0779 100644 --- a/AlgebraicDataflowArchitectureModel/models/WOS.dtram +++ b/AlgebraicDataflowArchitectureModel/models/WOS.dtram @@ -1,17 +1,17 @@ model { channel CIO2 { - out highest(h:Double, reset(v)) == v + out highest(h:Double, reset(v)) = v } channel CIO1 { - out temp_f(p:Double, observe(x)) == x + out temp_f(p:Double, observe(x)) = x } channel C1{ - in temp_f(q:Double, conversion(y)) == y - out temp_c(r:Double, conversion(z)) == (z-32) / 1.8 + in temp_f(q:Double, conversion(y)) = y + out temp_c(r:Double, conversion(z)) = (z-32) / 1.8 } channel C2{ - in temp_f(q:Double, update(y)) == y - out highest(h:Double, update(z)) == if(gt(z, h), z, h) + in temp_f(q:Double, update(y)) = y + out highest(h:Double, update(z)) = if(z >= h, z, h) } } geometry { diff --git a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model index 2cd84d7..0096407 100644 --- a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model +++ b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model @@ -1,14 +1,14 @@ channel CIO2 { - out highest(h:Double, reset(v)) == v + out highest(h:Double, reset(v)) = v } channel CIO1 { - out temp_f(p:Double, observe(x)) == x + out temp_f(p:Double, observe(x)) = x } channel C1{ - in temp_f(q:Double, conversion(y)) == y - out temp_c(r:Double, conversion(z)) == (z-32) / 1.8 + in temp_f(q:Double, conversion(y)) = y + out temp_c(r:Double, conversion(z)) = (z-32) / 1.8 } channel C2{ - in temp_f(q:Double, update(y)) == y - out highest(h:Double, update(z)) == if(gt(z, h), z, h) + in temp_f(q:Double, update(y)) = y + out highest(h:Double, update(z)) = if(z >= h, z, h) } diff --git a/AlgebraicDataflowArchitectureModel/src/models/algebra/Constant.java b/AlgebraicDataflowArchitectureModel/src/models/algebra/Constant.java index cc1ffee..5f533a7 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/algebra/Constant.java +++ b/AlgebraicDataflowArchitectureModel/src/models/algebra/Constant.java @@ -36,7 +36,7 @@ public String toImplementation(String[] sideEffects) { if (symbol.isImplGenerative()) { - String exp = symbol.generate(getType(), new String[] {}, new String[] {}, sideEffects); + String exp = symbol.generate(getType(), new Type[] {}, new String[] {}, new String[] {}, sideEffects); return exp; } return symbol.getImplName(); diff --git a/AlgebraicDataflowArchitectureModel/src/models/algebra/LambdaAbstraction.java b/AlgebraicDataflowArchitectureModel/src/models/algebra/LambdaAbstraction.java new file mode 100644 index 0000000..9898224 --- /dev/null +++ b/AlgebraicDataflowArchitectureModel/src/models/algebra/LambdaAbstraction.java @@ -0,0 +1,30 @@ +package models.algebra; + +import java.util.ArrayList; +import java.util.List; + +public class LambdaAbstraction extends Symbol { + private List variables = null; + private Term term = null; + + public LambdaAbstraction(Variable variable, Term term) { + super("($" + variable.getName() + ")->" + term.toString(), 1, Type.LAMBDA); + this.variables = new ArrayList<>(); + this.variables.add(variable); + this.term = term; + } + + public LambdaAbstraction(List variables, Term term) { + super("($" + variables + ")->" + term.toString(), variables.size(), Type.LAMBDA); + this.variables = variables; + this.term = term; + } + + public List getVariables() { + return variables; + } + + public Term getTerm() { + return term; + } +} diff --git a/AlgebraicDataflowArchitectureModel/src/models/algebra/Symbol.java b/AlgebraicDataflowArchitectureModel/src/models/algebra/Symbol.java index 5a06873..ec1442e 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/algebra/Symbol.java +++ b/AlgebraicDataflowArchitectureModel/src/models/algebra/Symbol.java @@ -1,15 +1,15 @@ package models.algebra; public class Symbol { - private String name; - private String implName; - private int arity = 0; // -1: variable number - private Type operatorType = Type.PREFIX; - private Type implOperatorType = Type.PREFIX; - private Symbol[] inverses = null; - private models.algebra.Type[] signature = null; - private int[] implParamOrder = null; - private IImplGenerator generator = null; + protected String name; + protected String implName; + protected int arity = 0; // -1: variable number + protected Type operatorType = Type.PREFIX; + protected Type implOperatorType = Type.PREFIX; + protected Symbol[] inverses = null; + protected models.algebra.Type[] signature = null; + protected int[] implParamOrder = null; + protected IImplGenerator generator = null; public Symbol(String name) { this.name = name; @@ -89,6 +89,10 @@ public boolean isMethod() { return (operatorType == Type.METHOD || operatorType == Type.METHOD_WITH_SIDE_EFFECT); } + + public boolean isLambda() { + return (operatorType == Type.LAMBDA); + } public Symbol[] getInverses() { return inverses; @@ -155,14 +159,15 @@ /** * Generate the implementation of this symbol * @param type the type of this symbol + * @param childrenTypes the types of the children expressions * @param childrenImpl the implementations of the children * @param childrenSideEffects (input) an array of the side effects of the children * @param sideEffect (output) an array of the side effect of this symbol * @return the implementation */ - public String generate(models.algebra.Type type, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + public String generate(models.algebra.Type type, models.algebra.Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { if (generator != null) { - return generator.generate(type, childrenImpl, childrenSideEffects, sideEffect); + return generator.generate(type, childrenTypes, childrenImpl, childrenSideEffects, sideEffect); } return null; } @@ -224,6 +229,6 @@ * @param sideEffect (output) an array of the side effect of this generator * @return the generated implementation */ - public String generate(models.algebra.Type type, String children[], String[] childrenSideEffects, String[] sideEffect); + public String generate(models.algebra.Type type, models.algebra.Type[] childrenTypes, String children[], String[] childrenSideEffects, String[] sideEffect); } } diff --git a/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java b/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java index 13c9969..4d5d7e2 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java +++ b/AlgebraicDataflowArchitectureModel/src/models/algebra/Term.java @@ -1,12 +1,14 @@ package models.algebra; import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; +import java.util.List; import java.util.Map.Entry; public class Term extends Expression { protected Symbol symbol = null; - protected ArrayList children = new ArrayList<>(); + protected List children = new ArrayList<>(); protected Type type = null; public Term(Symbol symbol) { @@ -14,12 +16,18 @@ this.symbol = symbol; } - public Term(Symbol symbol, ArrayList children) { + public Term(Symbol symbol, List children) { super(); this.symbol = symbol; this.children = children; } + public Term(Symbol symbol, Expression[] children) { + super(); + this.symbol = symbol; + this.children = new ArrayList<>(Arrays.asList(children)); + } + public Symbol getSymbol() { return symbol; } @@ -55,7 +63,7 @@ return children.get(n); } - public ArrayList getChildren() { + public List getChildren() { return children; } @@ -123,6 +131,55 @@ } } + public Expression reduce() { + if (symbol.isLambda()) { + // Lambda beta-reduction + LambdaAbstraction newSymbol = ((LambdaAbstraction) symbol); + Term newTerm = newSymbol.getTerm(); + List newVariables = newSymbol.getVariables(); + List newChildren = children; + while (newVariables.size() > 0 && newChildren.size() > 0) { + newTerm = newTerm.substitute(newVariables.get(0), newChildren.get(0)); + newVariables = newVariables.subList(1, newVariables.size()); + newChildren = newChildren.subList(1, newChildren.size()); + newSymbol = new LambdaAbstraction(newVariables, newTerm); + } + if (newSymbol.arity == 0 && newChildren.size() == 0) { + return newTerm; + } else { + return new Term(newSymbol, newChildren); + } + } else { + // Calculate inverse map + List newChildren = new ArrayList<>(); + boolean bReduced = false; + for (Expression child: children) { + if (child instanceof Term && !(child instanceof Constant)) { + child = ((Term) (child)).reduce(); + bReduced = true; + } + newChildren.add(child); + } + if (symbol.arity == 1 && newChildren.size() == 1) { + Expression child = newChildren.get(0); + if (child instanceof Term && !(child instanceof Constant)) { + Symbol childSymbol = ((Term) child).getSymbol(); + if (childSymbol.getInverses() != null) { + for (int i = 0; i < childSymbol.getInverses().length; i++) { + if (symbol.equals(childSymbol.getInverses()[i])) { + return ((Term) child).getChild(i); + } + } + } + } + } + if (!bReduced) return this; + Term newTerm = new Term(symbol, newChildren); + newTerm.setType(type); + return newTerm; + } + } + @Override public Expression getInverseMap(Expression outputValue, Position targetPos) { if (targetPos.isEmpty()) return outputValue; @@ -233,15 +290,22 @@ return exp; } if (symbol.isImplGenerative()) { + Type childrenTypes[] = new Type[children.size()]; String childrenImpl[] = new String[children.size()]; String childrenSideEffects[] = new String[children.size()]; if (implParamOrder == null) { for (int i = 0; i < children.size(); i++) { + Expression child = children.get(i); + if (child instanceof Variable) { + childrenTypes[i] = ((Variable) child).getType(); + } else if (child instanceof Term) { + childrenTypes[i] = ((Term) child).getType(); + } String childSideEffect[] = new String[] {""}; childrenImpl[i] = children.get(i).toImplementation(childSideEffect); childrenSideEffects[i] = childSideEffect[0]; } - String exp = symbol.generate(getType(), childrenImpl, childrenSideEffects, sideEffects); + String exp = symbol.generate(getType(), childrenTypes, childrenImpl, childrenSideEffects, sideEffects); if (symbol.isImplWithSideEffect()) { sideEffects[0] = sideEffects[0] + exp; exp = children.get(0).toImplementation(new String[] {""}); // the value of this term @@ -249,11 +313,17 @@ return exp; } else { for (int i = 0; i < children.size(); i++) { + Expression child = children.get(implParamOrder[i]); + if (child instanceof Variable) { + childrenTypes[i] = ((Variable) child).getType(); + } else if (child instanceof Term) { + childrenTypes[i] = ((Term) child).getType(); + } String childSideEffect[] = new String[] {""}; childrenImpl[i] = children.get(implParamOrder[i]).toImplementation(childSideEffect); childrenSideEffects[i] = childSideEffect[0]; } - String exp = symbol.generate(getType(), childrenImpl, childrenSideEffects, sideEffects); + String exp = symbol.generate(getType(), childrenTypes, childrenImpl, childrenSideEffects, sideEffects); if (symbol.isImplWithSideEffect()) { sideEffects[0] = sideEffects[0] + exp; exp = children.get(implParamOrder[0]).toImplementation(new String[] {""}); // the value of this term diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/ChannelMember.java b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/ChannelMember.java index 190a49f..af7f386 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/ChannelMember.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/ChannelMember.java @@ -53,6 +53,6 @@ return resourcePath.getResourceName() + "(" + stateTransition.getCurStateExpression() + "," + stateTransition.getMessageExpression() + ")" - + " == " + stateTransition.getNextStateExpression(); + + " = " + stateTransition.getNextStateExpression(); } } diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java index 75850b9..c2ce3fd 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java @@ -3,8 +3,12 @@ import java.util.Collection; import java.util.HashMap; +import models.algebra.Expression; +import models.algebra.LambdaAbstraction; import models.algebra.Symbol; +import models.algebra.Term; import models.algebra.Type; +import models.algebra.Variable; import parser.Parser; public class DataConstraintModel { @@ -33,6 +37,16 @@ public static final Symbol sub = new Symbol(Parser.SUB, 2, Symbol.Type.INFIX); public static final Symbol div = new Symbol(Parser.DIV, 2, Symbol.Type.INFIX); public static final Symbol minus = new Symbol(Parser.MINUS, 1); + public static final Symbol mod = new Symbol(Parser.MOD, 2, Symbol.Type.INFIX, "%", Symbol.Type.INFIX); + public static final Symbol eq = new Symbol(Parser.EQ, 2, Symbol.Type.INFIX, "==", Symbol.Type.INFIX); + public static final Symbol neq = new Symbol(Parser.NEQ, 2, Symbol.Type.INFIX, "!=", Symbol.Type.INFIX); + public static final Symbol gt = new Symbol(Parser.GT, 2, Symbol.Type.INFIX, ">", Symbol.Type.INFIX); + public static final Symbol lt = new Symbol(Parser.LT, 2, Symbol.Type.INFIX, "<", Symbol.Type.INFIX); + public static final Symbol ge = new Symbol(Parser.GE, 2, Symbol.Type.INFIX, ">=", Symbol.Type.INFIX); + public static final Symbol le = new Symbol(Parser.LE, 2, Symbol.Type.INFIX, "<=", Symbol.Type.INFIX); + public static final Symbol and = new Symbol(Parser.AND, 2, Symbol.Type.INFIX, "&&", Symbol.Type.INFIX); + public static final Symbol or = new Symbol(Parser.OR, 2, Symbol.Type.INFIX, "||", Symbol.Type.INFIX); + public static final Symbol neg = new Symbol(Parser.NEG, 1, Symbol.Type.INFIX, "!", Symbol.Type.PREFIX); public static final Symbol cons = new Symbol("cons", 2, Symbol.Type.PREFIX, "($x,$y)->$x.add(0, $y)", Symbol.Type.LAMBDA_WITH_SIDE_EFFECT, new int[] {1, 0}); public static final Symbol append = new Symbol("append", 2, Symbol.Type.PREFIX, "add", Symbol.Type.METHOD_WITH_SIDE_EFFECT); public static final Symbol remove = new Symbol("remove", 2, Symbol.Type.PREFIX, "remove", Symbol.Type.METHOD_WITH_SIDE_EFFECT); @@ -41,10 +55,21 @@ public static final Symbol length = new Symbol("length", 1, Symbol.Type.PREFIX, "($x)->$x.size()", Symbol.Type.LAMBDA); public static final Symbol get = new Symbol("get", 2, Symbol.Type.PREFIX, "get", Symbol.Type.METHOD); public static final Symbol set = new Symbol("set", 3, Symbol.Type.PREFIX, "set", Symbol.Type.METHOD_WITH_SIDE_EFFECT); - public static final Symbol contains = new Symbol("contains", 2, Symbol.Type.PREFIX, "contains", Symbol.Type.METHOD); + public static final Symbol contains = new Symbol("contains", 2, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { + @Override + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + for (String s: childrenSideEffects) { + sideEffect[0] += s; + } + if (childrenTypes[0] != null && typeMap.isAncestorOf(childrenTypes[0])) { + return childrenImpl[0] + "." + "containsKey(" + childrenImpl[1] + ")"; + } + return childrenImpl[0] + "." + "contains(" + childrenImpl[1] + ")"; + } + }); public static final Symbol nil = new Symbol("nil", 0, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] children, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String compType = ""; if (type != null) { String temp = "temp_nil"; @@ -63,21 +88,23 @@ } }); public static final Symbol null_ = new Symbol("null", 0, Symbol.Type.PREFIX, "null", Symbol.Type.PREFIX); + public static final Symbol true_ = new Symbol("true", 0, Symbol.Type.PREFIX, "true", Symbol.Type.PREFIX); + public static final Symbol false_ = new Symbol("false", 0, Symbol.Type.PREFIX, "false", Symbol.Type.PREFIX); public static final Symbol cond = new Symbol("if", 3, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { final int count[] = {0}; @Override - public String generate(Type type, String[] children, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String temp = "temp_if" + count[0]; String impl = ""; impl += type.getInterfaceTypeName() + " " + temp + ";\n"; if (childrenSideEffects[0] != null && childrenSideEffects[0].length() > 0) impl += childrenSideEffects[0]; - impl += "if (" + children[0] + ") {\n"; + impl += "if (" + childrenImpl[0] + ") {\n"; if (childrenSideEffects[1] != null && childrenSideEffects[1].length() > 0) impl += "\t" + childrenSideEffects[1]; - impl += "\t" + temp + " = " + children[1] + ";\n"; + impl += "\t" + temp + " = " + childrenImpl[1] + ";\n"; impl += "} else {\n"; if (childrenSideEffects[2] != null && childrenSideEffects[2].length() > 0) impl += "\t" + childrenSideEffects[2]; - impl += "\t" + temp + " = " + children[2] + ";\n"; + impl += "\t" + temp + " = " + childrenImpl[2] + ";\n"; impl += "}\n"; sideEffect[0] += impl; @@ -85,24 +112,10 @@ count[0]++; return temp; } - }); - - - public static final Symbol mod = new Symbol("mod", 2, Symbol.Type.PREFIX, "%", Symbol.Type.INFIX); - public static final Symbol eq = new Symbol("eq", 2, Symbol.Type.PREFIX, "==", Symbol.Type.INFIX); - public static final Symbol neq = new Symbol("neq", 2, Symbol.Type.PREFIX, "!=", Symbol.Type.INFIX); - public static final Symbol gt = new Symbol("gt", 2, Symbol.Type.PREFIX, ">", Symbol.Type.INFIX); - public static final Symbol lt = new Symbol("lt", 2, Symbol.Type.PREFIX, "<", Symbol.Type.INFIX); - public static final Symbol ge = new Symbol("ge", 2, Symbol.Type.PREFIX, ">=", Symbol.Type.INFIX); - public static final Symbol le = new Symbol("le", 2, Symbol.Type.PREFIX, "<=", Symbol.Type.INFIX); - public static final Symbol and = new Symbol("and", 2, Symbol.Type.PREFIX, "&&", Symbol.Type.INFIX); - public static final Symbol or = new Symbol("or", 2, Symbol.Type.PREFIX, "||", Symbol.Type.INFIX); - public static final Symbol neg = new Symbol("neg", 1, Symbol.Type.PREFIX, "!", Symbol.Type.PREFIX); - public static final Symbol true_ = new Symbol("true", 0, Symbol.Type.PREFIX, "true", Symbol.Type.PREFIX); - public static final Symbol false_ = new Symbol("false", 0, Symbol.Type.PREFIX, "false", Symbol.Type.PREFIX); + }); public static final Symbol pair = new Symbol("pair", -1, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { for (String s: childrenSideEffects) { sideEffect[0] += s; } @@ -112,7 +125,7 @@ }); public static final Symbol tuple = new Symbol("tuple", -1, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { for (String s: childrenSideEffects) { sideEffect[0] += s; } @@ -133,7 +146,7 @@ public static final Symbol lookup = new Symbol("lookup", 2, Symbol.Type.PREFIX, new Symbol.IImplGenerator() { final int count[] = {0}; @Override - public String generate(Type type, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String temp = "temp_get" + count[0]; String impl = childrenSideEffects[0] + childrenSideEffects[1]; impl += type.getInterfaceTypeName() + " " + temp + ";\n"; @@ -168,16 +181,6 @@ div.setInverses(new Symbol[] {mul}); minus.setInverses(new Symbol[] {minus}); mod.setSignature(new Type[] {typeInt, null, null}); - cons.setInverses(new Symbol[] {head, tail}); - cons.setSignature(new Type[] {typeList, null, typeList}); - append.setSignature(new Type[] {typeList, typeList, null}); - remove.setSignature(new Type[] {typeList, typeList, typeInt}); - head.setSignature(new Type[] {null, typeList}); - tail.setSignature(new Type[] {typeList, typeList}); - contains.setSignature(new Type[] {typeBoolean, typeList, null}); - length.setSignature(new Type[] {typeInt, null}); - get.setSignature(new Type[] {null, typeList, typeInt}); - set.setSignature(new Type[] {typeList, typeList, typeInt, null}); eq.setSignature(new Type[] {typeBoolean, null, null}); neq.setSignature(new Type[] {typeBoolean, null, null}); gt.setSignature(new Type[] {typeBoolean, null, null}); @@ -187,9 +190,19 @@ and.setSignature(new Type[] {typeBoolean, typeBoolean, typeBoolean}); or.setSignature(new Type[] {typeBoolean, typeBoolean, typeBoolean}); neg.setSignature(new Type[] {typeBoolean, typeBoolean}); + cons.setInverses(new Symbol[] {head, tail}); + cons.setSignature(new Type[] {typeList, null, typeList}); + append.setSignature(new Type[] {typeList, typeList, null}); + remove.setSignature(new Type[] {typeList, typeList, typeInt}); + head.setSignature(new Type[] {null, typeList}); + tail.setSignature(new Type[] {typeList, typeList}); + contains.setSignature(new Type[] {typeBoolean, null, null}); + length.setSignature(new Type[] {typeInt, null}); + get.setSignature(new Type[] {null, typeList, typeInt}); + set.setSignature(new Type[] {typeList, typeList, typeInt, null}); + null_.setSignature(new Type[] {null}); true_.setSignature(new Type[] {typeBoolean}); false_.setSignature(new Type[] {typeBoolean}); - null_.setSignature(new Type[] {null}); pair.setSignature(new Type[] {typePair,null,null}); pair.setInverses(new Symbol[] {left, right}); left.setSignature(new Type[] {null, typePair}); @@ -197,7 +210,9 @@ tuple.setSignature(new Type[] {typeTuple, null, null}); tuple.setInverses(new Symbol[] {fst, snd}); fst.setSignature(new Type[] {null, typeTuple}); + fst.setInverses(new Symbol[] {new LambdaAbstraction(new Variable("x"), new Term(tuple, new Expression[] {new Variable("x"), new Variable("y")}))}); snd.setSignature(new Type[] {null, typeTuple}); + snd.setInverses(new Symbol[] {new LambdaAbstraction(new Variable("y"), new Term(tuple, new Expression[] {new Variable("x"), new Variable("y")}))}); insert.setSignature(new Type[] {typeMap, typeMap, null, null}); delete.setSignature(new Type[] {typeMap, typeMap, null}); lookup.setSignature(new Type[] {null, typeMap, null}); @@ -243,17 +258,6 @@ addSymbol(div); addSymbol(minus); addSymbol(mod); - addSymbol(cons); - addSymbol(append); - addSymbol(remove); - addSymbol(head); - addSymbol(tail); - addSymbol(length); - addSymbol(contains); - addSymbol(get); - addSymbol(set); - addSymbol(nil); - addSymbol(cond); addSymbol(eq); addSymbol(neq); addSymbol(gt); @@ -263,9 +267,20 @@ addSymbol(and); addSymbol(or); addSymbol(neg); + addSymbol(cons); + addSymbol(append); + addSymbol(remove); + addSymbol(head); + addSymbol(tail); + addSymbol(length); + addSymbol(contains); + addSymbol(get); + addSymbol(set); + addSymbol(cond); + addSymbol(nil); + addSymbol(null_); addSymbol(true_); addSymbol(false_); - addSymbol(null_); addSymbol(pair); addSymbol(left); addSymbol(right); diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/StateTransition.java b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/StateTransition.java index c8b939e..3762896 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/StateTransition.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/StateTransition.java @@ -4,6 +4,7 @@ import java.util.HashMap; import java.util.Map.Entry; +import models.algebra.Constant; import models.algebra.Expression; import models.algebra.InvalidMessage; import models.algebra.Position; @@ -69,6 +70,9 @@ Position varPos = curStateVarEnt.getKey(); Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos); if (valueCalc != null) { + if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) { + valueCalc = ((Term) valueCalc).reduce(); + } ArrayList values = bindings.get(var); if (values == null) { values = new ArrayList(); @@ -98,6 +102,9 @@ Position varPos = nextStateVarEnt.getKey(); Expression valueCalc = nextStateTerm.getInverseMap(nextStateValue, varPos); if (valueCalc != null) { + if (valueCalc instanceof Term) { + valueCalc = ((Term) valueCalc).reduce(); + } ArrayList values = bindings.get(var); if (values == null) { values = new ArrayList(); @@ -108,12 +115,18 @@ } Expression messageTerm = getMessageExpression(); - if (!(messageTerm instanceof Term)) throw new InvalidMessage(); + if (!(messageTerm instanceof Term) && !(messageTerm instanceof Variable)) throw new InvalidMessage(); HashMap messageVars = messageTerm.getVariables(); for (Variable var: messageVars.values()) { if (bindings.get(var) != null) { if (bindings.get(var).size() > 1) throw new ResolvingMultipleDefinitionIsFutureWork(); - messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next()); + if (messageTerm instanceof Term) { + messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next()); + } else if (messageTerm instanceof Variable) { + if (messageTerm.equals(var)) { + return bindings.get(var).iterator().next(); + } + } } } return messageTerm; @@ -129,6 +142,9 @@ Position varPos = curStateVarEnt.getKey(); Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos); if (valueCalc != null) { + if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) { + valueCalc = ((Term) valueCalc).reduce(); + } ArrayList values = bindings.get(var); if (values == null) { values = new ArrayList(); @@ -139,12 +155,18 @@ } Expression messageTerm = getMessageExpression(); - if (!(messageTerm instanceof Term)) throw new InvalidMessage(); + if (!(messageTerm instanceof Term) && !(messageTerm instanceof Variable)) throw new InvalidMessage(); HashMap messageVars = messageTerm.getVariables(); for (Variable var: messageVars.values()) { if (bindings.get(var) != null) { if (bindings.get(var).size() > 1) throw new ResolvingMultipleDefinitionIsFutureWork(); - messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next()); + if (messageTerm instanceof Term) { + messageTerm = ((Term) messageTerm).substitute(var, bindings.get(var).iterator().next()); + } else if (messageTerm instanceof Variable) { + if (messageTerm.equals(var)) { + return bindings.get(var).iterator().next(); + } + } } } return messageTerm; @@ -161,6 +183,9 @@ Position varPos = curStateVarEnt.getKey(); Expression valueCalc = curStateTerm.getInverseMap(curStateValue, varPos); if (valueCalc != null) { + if (valueCalc instanceof Term && !(valueCalc instanceof Constant)) { + valueCalc = ((Term) valueCalc).reduce(); + } if (bindings.get(var) != null) throw new ResolvingMultipleDefinitionIsFutureWork(); bindings.put(var, valueCalc); } @@ -189,6 +214,9 @@ nextStateTerm = ((Term) nextStateTerm).substitute(var, bindings.get(var)); } } + if (nextStateTerm instanceof Term && !(nextStateTerm instanceof Constant)) { + nextStateTerm = ((Term) nextStateTerm).reduce(); + } return nextStateTerm; } } diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataFlowModel/ModelExtension.java b/AlgebraicDataflowArchitectureModel/src/models/dataFlowModel/ModelExtension.java index 7d4ce1b..cffe1cb 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataFlowModel/ModelExtension.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataFlowModel/ModelExtension.java @@ -26,7 +26,7 @@ final int[] count = new int[] {0}; sum.setGenerator(new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] children, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String compType = "Integer"; if (type != null) { String interfaceType = type.getInterfaceTypeName(); @@ -36,7 +36,7 @@ } count[0]++; String impl = compType + " " + "temp_sum" + count[0] + " = 0;\n"; - impl += "for (" + compType + " x: " + children[0] + ") {\n"; + impl += "for (" + compType + " x: " + childrenImpl[0] + ") {\n"; impl += "\t" + "temp_sum" + count[0] + " += x;\n"; impl += "}\n"; sideEffect[0] = sideEffect[0] + impl; @@ -56,7 +56,7 @@ final int[] count = new int[] {0}; merge.setGenerator(new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String implType = "ArrayList<>"; String interfaceType = "List"; String compType = "Integer"; @@ -109,8 +109,8 @@ extractFaceDown.setArity(1); extractFaceDown.setGenerator(new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] children, String[] childrenSideEffects, String[] sideEffect) { - return children[0]+".stream().filter(item -> item.getValue()==false).collect(Collectors.toList())"; + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { + return childrenImpl[0]+".stream().filter(item -> item.getValue()==false).collect(Collectors.toList())"; } }); extractFaceDown.setImplOperatorType(Symbol.Type.GENERATIVE); @@ -124,7 +124,7 @@ sortByKey.setArity(1); sortByKey.setGenerator(new Symbol.IImplGenerator() { @Override - public String generate(Type type, String[] children, String[] childrenSideEffects, String[] sideEffect) { + public String generate(Type type, Type[] childrenTypes, String[] childrenImpl, String[] childrenSideEffects, String[] sideEffect) { String compType = ""; String temp_sort="temp_sort"; if (type != null) { @@ -141,7 +141,7 @@ for (String s: childrenSideEffects) { sideEffect[0] += s; } - temp_sort=children[0]+".sort(Comparator.comparing("+compType+"::getKey));\n"; + temp_sort=childrenImpl[0]+".sort(Comparator.comparing("+compType+"::getKey));\n"; return temp_sort; } }); diff --git a/AlgebraicDataflowArchitectureModel/src/models/visualModel/FormulaChannel.java b/AlgebraicDataflowArchitectureModel/src/models/visualModel/FormulaChannel.java index 581d31e..1e09595 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/visualModel/FormulaChannel.java +++ b/AlgebraicDataflowArchitectureModel/src/models/visualModel/FormulaChannel.java @@ -63,8 +63,8 @@ super.addChannelMemberAsOutput(channelMember); if (getOutputChannelMembers().size() == 1) { if (formula == null) formula = ""; - if (!formula.contains("==")) { - formula = channelMember.getResource().getResourceName() + " == " + formula; + if (!formula.contains("=")) { + formula = channelMember.getResource().getResourceName() + " = " + formula; } } if (formulaRhs != null) { diff --git a/AlgebraicDataflowArchitectureModel/src/parser/Parser.java b/AlgebraicDataflowArchitectureModel/src/parser/Parser.java index 0ec0f5a..d319d63 100644 --- a/AlgebraicDataflowArchitectureModel/src/parser/Parser.java +++ b/AlgebraicDataflowArchitectureModel/src/parser/Parser.java @@ -1,6 +1,5 @@ package parser; -import java.awt.image.DataBufferDouble; import java.io.BufferedReader; import java.io.IOException; import java.util.ArrayList; @@ -47,7 +46,17 @@ public static final String MUL = "*"; public static final String SUB = "-"; public static final String DIV = "/"; + public static final String MOD = "%"; public static final String MINUS = "-"; + public static final String EQ = "=="; + public static final String NEQ = "!="; + public static final String GT = ">"; + public static final String LT = "<"; + public static final String GE = ">="; + public static final String LE = "<="; + public static final String AND = "&&"; + public static final String OR = "||"; + public static final String NEG = "!"; public static final String ADD_REGX = "\\+"; public static final String MUL_REGX = "\\*"; public static final String SUB_REGX = "\\-"; @@ -55,7 +64,8 @@ public static final String IN = "in"; public static final String OUT = "out"; public static final String REF = "ref"; - public static final String EQUALS = "=="; + public static final String OR_REGX = "\\|\\|"; + public static final String EQUALS = "="; public static final String ASSIGNMENT = "="; public static final String COMMA = ","; public static final String COLON = ":"; @@ -246,20 +256,23 @@ ArrayList operators = new ArrayList<>(); String operator = null; for (;;) { - String leftBracketOrMinus = stream.next(); - if (leftBracketOrMinus.equals(LEFT_BRACKET)) { + String leftBracketOrMinusOrNeg = stream.next(); + if (leftBracketOrMinusOrNeg.equals(LEFT_BRACKET)) { Expression exp = parseTerm(stream, model); String rightBracket = stream.next(); if (!rightBracket.equals(RIGHT_BRACKET)) throw new ExpectedRightBracket(stream.getLine()); expressions.add(exp); } else { - Symbol minus = null; + Symbol minusOrNeg = null; String symbolName = null; - if (leftBracketOrMinus.equals(MINUS)) { - minus = DataTransferModel.minus; // not sub + if (leftBracketOrMinusOrNeg.equals(MINUS)) { + minusOrNeg = DataTransferModel.minus; // not sub + symbolName = stream.next(); + } else if (leftBracketOrMinusOrNeg.equals(NEG)) { + minusOrNeg = DataTransferModel.neg; symbolName = stream.next(); } else { - symbolName = leftBracketOrMinus; + symbolName = leftBracketOrMinusOrNeg; } Expression exp = null; if (stream.checkNext() != null && stream.checkNext().equals(LEFT_BRACKET)) { @@ -317,10 +330,10 @@ } } } - if (minus != null) { - Term minusTerm = new Term(minus); - minusTerm.addChild(exp); - expressions.add(minusTerm); + if (minusOrNeg != null) { + Term minusOrNegTerm = new Term(minusOrNeg); + minusOrNegTerm.addChild(exp); + expressions.add(minusOrNegTerm); } else { expressions.add(exp); } @@ -330,16 +343,49 @@ break; } else if (operator.equals(ADD)) { operators.add(DataTransferModel.add); + stream.next(); } else if (operator.equals(MUL)) { operators.add(DataTransferModel.mul); + stream.next(); } else if (operator.equals(SUB)) { operators.add(DataTransferModel.sub); // not minus + stream.next(); } else if (operator.equals(DIV)) { operators.add(DataTransferModel.div); + stream.next(); + } else if (operator.equals(MOD)) { + operators.add(DataTransferModel.mod); + stream.next(); + } else if (operator.equals(EQ)) { + operators.add(DataTransferModel.eq); + stream.next(); + } else if (operator.equals(NEQ)) { + operators.add(DataTransferModel.neq); + stream.next(); + } else if (operator.equals(GT)) { + operators.add(DataTransferModel.gt); + stream.next(); + } else if (operator.equals(LT)) { + operators.add(DataTransferModel.lt); + stream.next(); + } else if (operator.equals(GE)) { + operators.add(DataTransferModel.ge); + stream.next(); + } else if (operator.equals(LE)) { + operators.add(DataTransferModel.le); + stream.next(); + } else if (operator.equals(AND)) { + operators.add(DataTransferModel.and); + stream.next(); + } else if (operator.equals(OR)) { + operators.add(DataTransferModel.or); + stream.next(); + } else if (operator.equals(NEG)) { + operators.add(DataTransferModel.neg); + stream.next(); } else { break; } - stream.next(); // an arithmetic operator } if (expressions.size() == 1) { // no arithmetic operators @@ -351,7 +397,9 @@ int i = 1; for (Symbol op: operators) { Expression second = expressions.get(i); - if (op.getName().equals(MUL) || op.getName().equals(DIV)) { + if (op.getName().equals(MUL) || op.getName().equals(DIV) || op.getName().equals(MOD) + || op.getName().equals(EQ) || op.getName().equals(NEQ) || op.getName().equals(GT) || op.getName().equals(LT) + || op.getName().equals(GE) || op.getName().equals(LE) || op.getName().equals(AND) || op.getName().equals(OR)) { Term term = new Term(op); term.addChild(first); term.addChild(second); @@ -397,7 +445,7 @@ * "TokenStream" has a token what is read from description of "Architecture Language Model". */ public static class TokenStream { - private ArrayList> tokens = new ArrayList<>(); + private ArrayList> tokens = new ArrayList<>(); private ArrayList lines = new ArrayList<>(); private int line = 0; private int n = 0; @@ -422,15 +470,45 @@ splitBy( splitBy( splitBy( - Arrays.asList(line.split("[ \t]")), - ADD, - ADD_REGX), - MUL, - MUL_REGX), - SUB, - SUB_REGX), - DIV, - DIV_REGX), + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + splitBy( + line.split("[ \t]"), + ADD, + ADD_REGX), + MUL, + MUL_REGX), + SUB, + SUB_REGX), + DIV, + DIV_REGX), + MOD, + MOD), + EQ, + EQ), + NEQ, + NEQ), + GE, + GE), + LE, + LE), + GT, + GT), + LT, + LT), + AND, + AND), + OR, + OR_REGX), + NEG, + NEG), COMMA, COMMA), COLON, @@ -447,23 +525,35 @@ RIGHT_CURLY_BRACKET_REGX)); } - private ArrayList splitBy(final List tokens, final String delimiter, final String delimiterRegx) { - ArrayList newTokens = new ArrayList<>(); + private ArrayList splitBy(String[] tokens, final String delimiter, final String delimiterRegx) { + ArrayList newTokens = new ArrayList<>(); for (String token: tokens) { - String[] splitTokens = token.split(delimiterRegx); - boolean fFirstToken = true; - for (String t: splitTokens) { - if (!fFirstToken) { - newTokens.add(delimiter); + newTokens.add(new Token(token)); + } + return splitBy(newTokens, delimiter, delimiterRegx); + } + + private ArrayList splitBy(final List tokens, final String delimiter, final String delimiterRegx) { + ArrayList newTokens = new ArrayList<>(); + for (Token token: tokens) { + if (token.isAtomic()) { + newTokens.add(token); + } else { + String[] splitTokens = token.split(delimiterRegx); + boolean fFirstToken = true; + for (String t: splitTokens) { + if (!fFirstToken) { + newTokens.add(new Token(delimiter, true)); + } + if (t.length() > 0) { + newTokens.add(new Token(t)); + } + fFirstToken = false; } - if (t.length() > 0) { - newTokens.add(t); + while (token.endsWith(delimiter)) { + newTokens.add(new Token(delimiter, true)); + token = token.substring(0, token.length() - 1); } - fFirstToken = false; - } - while (token.endsWith(delimiter)) { - newTokens.add(delimiter); - token = token.substring(0, token.length() - 1); } } return newTokens; @@ -476,7 +566,7 @@ n = 0; if (line >= tokens.size()) return null; } - String token = tokens.get(line).get(n); + String token = tokens.get(line).get(n).getTokenStr(); n++; return token; } @@ -488,7 +578,7 @@ n = 0; if (line >= tokens.size()) return null; } - return tokens.get(line).get(n); + return tokens.get(line).get(n).getTokenStr(); } public boolean hasNext() { @@ -513,4 +603,42 @@ return text; } } + + public static class Token { + String token; + boolean isAtomic = false; + + public Token(String token) { + this.token = token; + } + + public Token(String token, boolean isAtomic) { + this.token = token; + this.isAtomic = isAtomic; + } + + public String getTokenStr() { + return token; + } + + public boolean isAtomic() { + return isAtomic; + } + + public String[] split(String delimiterRegx) { + return token.split(delimiterRegx); + } + + public boolean endsWith(String delimiter) { + return token.endsWith(delimiter); + } + + public int length() { + return token.length(); + } + + public Token substring(int beginIdx, int endIdx) { + return new Token(token.substring(beginIdx, endIdx)); + } + } } diff --git a/AlgebraicDataflowArchitectureModel/src/tests/InverseTest.java b/AlgebraicDataflowArchitectureModel/src/tests/InverseTest.java index bfa8957..85644fc 100644 --- a/AlgebraicDataflowArchitectureModel/src/tests/InverseTest.java +++ b/AlgebraicDataflowArchitectureModel/src/tests/InverseTest.java @@ -14,6 +14,7 @@ import models.algebra.Expression; import models.algebra.Position; +import models.algebra.Term; import models.algebra.Variable; import models.dataFlowModel.DataTransferModel; import parser.Parser; @@ -23,9 +24,9 @@ public class InverseTest { @Test public void test() { - String lhs = "y"; DataTransferModel model = new DataTransferModel(); try { + String lhs = "y"; String rhs = "(a * x + b) * c"; TokenStream stream = new Parser.TokenStream(); @@ -33,7 +34,7 @@ stream.addLine(rhs); Expression rhsExp = parser.parseTerm(stream, model); - System.out.println(lhs + " = " + rhsExp); + System.out.println("=== solve{" + lhs + " = " + rhsExp + "} for a, b, d, x ==="); HashMap rhsVars = rhsExp.getVariables(); assertEquals(4, rhsVars.size()); @@ -47,6 +48,41 @@ assertFalse(inv.contains(v)); System.out.println(rhsVars.get(vPos) + " = " + inv); } + + // Extract an element in a tuple + TokenStream stream2 = new Parser.TokenStream(); + Parser parser2 = new Parser(stream2); + stream2.addLine("fst(tuple(x, y))"); + Expression tupleExp = parser2.parseTerm(stream2, model); + stream2.addLine("snd(tuple(x, y))"); + Expression tupleExp2 = parser2.parseTerm(stream2, model); + Expression reduced = ((Term) tupleExp).reduce(); + Expression reduced2 = ((Term) tupleExp2).reduce(); + Variable x = new Variable("x"); + assertEquals(reduced, x); + assertEquals(reduced2, y); + System.out.println("=== simplify ==="); + System.out.println(tupleExp + " = " + reduced); + System.out.println(tupleExp2 + " = " + reduced2); + + // Solve {z = fst(x)} for x + TokenStream stream3 = new Parser.TokenStream(); + Parser parser3 = new Parser(stream3); + stream3.addLine("fst(x)"); + Expression rhsExp3 = parser3.parseTerm(stream3, model); + Variable z = new Variable("z"); + System.out.println("=== solve{" + z + " = " + rhsExp3 + "} for x ==="); + HashMap rhsVars3 = rhsExp3.getVariables(); + for (Position vPos: rhsVars3.keySet()) { + Variable v = rhsVars3.get(vPos); + Expression inv = rhsExp3.getInverseMap(z, vPos); // inverse map to get v back from the output value y + if (inv instanceof Term) { + inv = ((Term) inv).reduce(); + } + assertTrue(inv.contains(z)); + assertFalse(inv.contains(v)); + System.out.println(rhsVars3.get(vPos) + " = " + inv); + } } catch (ExpectedRightBracket e) { e.printStackTrace(); } diff --git a/AlgebraicDataflowArchitectureModel/src/tests/SimplifiedDataFlowModelTest.java b/AlgebraicDataflowArchitectureModel/src/tests/SimplifiedDataFlowModelTest.java index acb5333..66befc7 100644 --- a/AlgebraicDataflowArchitectureModel/src/tests/SimplifiedDataFlowModelTest.java +++ b/AlgebraicDataflowArchitectureModel/src/tests/SimplifiedDataFlowModelTest.java @@ -21,7 +21,7 @@ // === cin === // - // payment(p1, purchase(x)) == x + // payment(p1, purchase(x)) = x // DataTransferChannel cin = new DataTransferChannel("cin"); ChannelMember cin_payment = new ChannelMember(payment); @@ -30,8 +30,8 @@ // === c1 === // - // payment(p1, update1(y)) == y - // loyalty(l, update1(y)) == floor(y * 0.05) + // payment(p1, update1(y)) = y + // loyalty(l, update1(y)) = floor(y * 0.05) // DataTransferChannel c1 = new DataTransferChannel("c1"); ChannelMember c1_payment = new ChannelMember(payment); @@ -44,8 +44,8 @@ // === c2 === // - // payment(p1, update2(z)) == z - // history(h, update2(z)) == cons(z, h) + // payment(p1, update2(z)) = z + // history(h, update2(z)) = cons(z, h) // DataTransferChannel c2 = new DataTransferChannel("c2"); ChannelMember c2_payment = new ChannelMember(payment); @@ -58,8 +58,8 @@ // === c3 === // - // history(h, update3(u)) == u - // total(t, update3(u)) == sum(u) + // history(h, update3(u)) = u + // total(t, update3(u)) = sum(u) // DataTransferChannel c3 = new DataTransferChannel("c3"); ChannelMember c3_history = new ChannelMember(history); diff --git a/AlgebraicDataflowArchitectureModel/src/tests/UpdateCodeGenerationTest.java b/AlgebraicDataflowArchitectureModel/src/tests/UpdateCodeGenerationTest.java index 69a5b1f..583dc89 100644 --- a/AlgebraicDataflowArchitectureModel/src/tests/UpdateCodeGenerationTest.java +++ b/AlgebraicDataflowArchitectureModel/src/tests/UpdateCodeGenerationTest.java @@ -105,8 +105,8 @@ // === c1 === // - // payment(p1, update1(y)) == y - // loyalty(l, update1(y)) == floor(y * 0.05) + // payment(p1, update1(y)) = y + // loyalty(l, update1(y)) = floor(y * 0.05) // DataTransferChannel c1 = new DataTransferChannel("c1"); ChannelMember c1_payment = new ChannelMember(payment); @@ -172,8 +172,8 @@ // === c2 === // - // payment(p1, update2(z)) == z - // history(h, update2(z)) == cons(z, h) + // payment(p1, update2(z)) = z + // history(h, update2(z)) = cons(z, h) // DataTransferChannel c2 = new DataTransferChannel("c2"); ChannelMember c2_payment = new ChannelMember(payment);