diff --git a/AlgebraicDataflowArchitectureModel/.classpath b/AlgebraicDataflowArchitectureModel/.classpath
index 3e99697..b969383 100644
--- a/AlgebraicDataflowArchitectureModel/.classpath
+++ b/AlgebraicDataflowArchitectureModel/.classpath
@@ -1,12 +1,12 @@
-
-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/AlgebraicDataflowArchitectureModel/.settings/org.eclipse.jdt.core.prefs b/AlgebraicDataflowArchitectureModel/.settings/org.eclipse.jdt.core.prefs
index 263a512..d0dc81b 100644
--- a/AlgebraicDataflowArchitectureModel/.settings/org.eclipse.jdt.core.prefs
+++ b/AlgebraicDataflowArchitectureModel/.settings/org.eclipse.jdt.core.prefs
@@ -1,9 +1,9 @@
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=13
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=14
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=13
+org.eclipse.jdt.core.compiler.compliance=14
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
@@ -12,4 +12,4 @@
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
org.eclipse.jdt.core.compiler.release=disabled
-org.eclipse.jdt.core.compiler.source=13
+org.eclipse.jdt.core.compiler.source=14
diff --git a/AlgebraicDataflowArchitectureModel/models/Accounts.model b/AlgebraicDataflowArchitectureModel/models/Accounts.model
new file mode 100644
index 0000000..cce8811
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Accounts.model
@@ -0,0 +1,6 @@
+channel CIO2(uid:Int) {
+ out accounts.{uid}.name(n:Str, changeName(name)) = name
+}
+channel CIO1 {
+ out accounts(l:List, signup(name:Str)) = append(l, {"name": name})
+}
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..8ea8dc2 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/CarRoad.model b/AlgebraicDataflowArchitectureModel/models/CarRoad.model
new file mode 100644
index 0000000..4822412
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/CarRoad.model
@@ -0,0 +1,48 @@
+init {
+ roads := {
+ "static": {
+ "road1": {
+ "left": "road2"
+ },
+ "road2": {
+ "right": "road1"
+ }
+ },
+ "dynamic": {
+ "road1": {
+ "left": nil,
+ "right": nil,
+ "straight": nil
+ },
+ "road2": {
+ "left": nil,
+ "right": nil,
+ "straight": nil
+ }
+ }
+ }
+}
+
+channel addVehicle {
+ out vehicles(vehicles: Map, addVehicle(id: Str, road: Str, turn: Str)) = insert(vehicles, id, {"road": road, "turn": turn, "nextTurn": ""})
+ out roads.dynamic.{road}.{turn}(roadVehicles: Map, addVehicle(id, road, turn)) = insert(raodVehicles, id, true)
+}
+
+channel turn(vid: Str){
+ out vehicles.{vid}.nextTurn(cur: Str, turn(next: Str)) = next
+}
+
+channel turn2 {
+ in vehicles.{vid}.nextTurn(cur: Str, turn2(nextTurn: Str, road: Str, turn: Str, nextRoad: Str)) = nextTurn
+ ref vehicles.{vid}.road(curRoad: Str, turn2(nextTurn, curRoad, turn, nextRoad))
+ ref vehicles.{vid}.turn(curTurn: Str, turn2(nextTurn, road, curTurn, nextRoad))
+ ref roads.static.{road}.{turn}(nextRoad: Str, turn2(nextTurn, road, turn, nextRoad))
+ out vehicles.{vid}.turn(cur: Str, turn2(nextTurn, road, turn, nextRoad)) = nextTurn
+ out roads.dynamic.{road}.{turn}.{vid}(curV: Bool, turn2(nextTurn, road, turn, nextRoad)) = false
+ out roads.dynamic.{nextRoad}.{nextTurn}(roadVehicles: Map, turn2(nextTurn, road, turn, nextRoad)) = insert(roadVehicles, vid, true)
+}
+
+
+
+
+
diff --git a/AlgebraicDataflowArchitectureModel/models/Citrus.model b/AlgebraicDataflowArchitectureModel/models/Citrus.model
new file mode 100644
index 0000000..356405a
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Citrus.model
@@ -0,0 +1,75 @@
+channel Signup {
+ out accounts(accDB:Map, signup(aid:Str)) = insert(accDB, aid, {"favorites": nil, "books": nil})
+}
+
+channel CreateBook(aid:Str) {
+ out accounts.{aid}.books(bookList:List, createBook(title:Str)) = append(bookList, {"title": title, "todos": nil, "favorited": nil})
+}
+
+channel DeleteAccount {
+ out accounts(accDB:Map, deleteAccount(aid:Str)) = if(contains(accDB, aid), delete(accDB, aid), accDB)
+}
+
+channel ChangeAccountName {
+ out accounts(accDB:Map, changeAccountId(aid:Str, newAid:Str)) = if(aid == newAid, accDB, delete(insert(accDB, newAid, lookup(accDB, aid)), aid))
+}
+
+channel ChangeBookName(aid:Str, bid:Int) {
+ out accounts.{aid}.books.{bid}.title(title:Str, changeBookName(newTitle)) = newTitle
+}
+
+channel DeleteBook(aid:Str) {
+ out accounts.{aid}.books(bookList:List, deleteBook(bid:Int)) = if(bid < length(bookList), remove(bookList, bid), bookList)
+}
+
+channel CreateToDo(aid:Str, bid:Int) {
+ out accounts.{aid}.books.{bid}.todos(toDoDB:Map, createtodo(year:Str, month:Str, day:Str, title:Str)) =
+ if(
+ contains(toDoDB,year),
+ if(
+ contains(lookup(toDoDB,year),month),
+ if(
+ contains(lookup(lookup(toDoDB,year),month),day),
+ insert(toDoDB,year,insert(lookup(toDoDB,year),month,insert(lookup(lookup(toDoDB,year),month),day,append(lookup(lookup(lookup(toDoDB,year),month),day),{"title":title,"check":false})))),
+ insert(toDoDB,year,insert(lookup(toDoDB,year),month,insert(lookup(lookup(toDoDB,year),month),day,append(nil,{"title":title,"check":false}))))
+ ),
+ insert(toDoDB,year,insert(lookup(toDoDB,year),month,insert(nil,day,append(nil,{"title":title,"check":false}))))
+ ),
+ insert(toDoDB,year,insert(nil,month,insert(nil,day,append(nil,{"title":title,"check":false}))))
+ )
+}
+
+channel ChangeToDoName(aid:Str, bid:Int, year:Str, month:Str, day:Str, tid:Int) {
+ out accounts.{aid}.books.{bid}.todos.{year}.{month}.{day}.{tid}.title(title:Str, changeToDoName(newTitle)) = newTitle
+}
+
+channel ChangeCheck(aid:Str, bid:Int, year:Str, month:Str, day:Str, tid:Int) {
+ out accounts.{aid}.books.{bid}.todos.{year}.{month}.{day}.{tid}.check(check:Bool, changeCheck(newCheck)) = newCheck
+}
+
+channel DeleteToDo(aid:Str, bid:Int) {
+ out accounts.{aid}.books.{bid}.todos(toDoDB:Map, deleteToDo(year:Str, month:Str, day:Str, tid:Int)) = insert(toDoDB,
+ year,
+ insert(lookup(toDoDB, year),
+ month,
+ insert(lookup(lookup(toDoDB, year), month),
+ day,
+ remove(lookup(lookup(lookup(toDoDB, year), month), day),
+ tid))))
+}
+
+channel AddFavorited(aid:Str, bid:Int) {
+ out accounts.{aid}.books.{bid}.favorited(faList:List, addFavorited(o_aid:Str)) = if(aid==o_aid,
+ faList,
+ if(contains(faList, o_aid),
+ remove(faList, indexOf(faList, o_aid)),
+ append(faList, o_aid)))
+ out accounts.{o_aid}.favorites(aDB:Map, addFavorited(o_aid:Str))
+ = if(aid==o_aid,
+ aDB,
+ if(contains(aDB, aid),
+ if(contains(lookup(aDB, aid), bid),
+ insert(aDB, aid, remove(lookup(aDB, aid), indexOf(lookup(aDB, aid), bid))),
+ insert(aDB, aid, append(lookup(aDB, aid), bid))),
+ insert(aDB, aid, append(nil, bid))))
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/Clock.dtram b/AlgebraicDataflowArchitectureModel/models/Clock.dtram
new file mode 100644
index 0000000..bbeb6dc
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Clock.dtram
@@ -0,0 +1,27 @@
+model {
+channel CIO1 {
+ out min(m: Int, tick) = (m + 1) % 60
+}
+channel HourUpdate {
+ in hour(h: Int, update(h2)) = h2
+ out hour_ang(h_ang: Double, update(h2)) = h2 / 6 * PI
+}
+channel MinUpdate {
+ in min(m, update(m2)) = m2
+ out min_ang(m_ang: Double, update(m2)) = m2 / 30 * PI
+}
+channel Clock {
+ in min(m, update(m2)) = m2
+ out hour(h, update(m2)) = if(m2 == 0, (h + 1) % 24, h)
+}
+}
+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/Clock.model b/AlgebraicDataflowArchitectureModel/models/Clock.model
new file mode 100644
index 0000000..0ecb11b
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Clock.model
@@ -0,0 +1,15 @@
+channel CIO1 {
+ out min(m: Int, tick) = (m + 1) % 60
+}
+channel HourUpdate {
+ in hour(h: Int, update(h2)) = h2
+ out hour_ang(h_ang: Double, update(h2)) = h2 / 6 * PI
+}
+channel MinUpdate {
+ in min(m, update(m2)) = m2
+ out min_ang(m_ang: Double, update(m2)) = m2 / 30 * PI
+}
+channel Clock {
+ in min(m, update(m2)) = m2
+ out hour(h, update(m2)) = if(m2 == 0, (h + 1) % 24, h)
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/CustomerManagement.model b/AlgebraicDataflowArchitectureModel/models/CustomerManagement.model
new file mode 100644
index 0000000..5277f32
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/CustomerManagement.model
@@ -0,0 +1,21 @@
+channel AddCustomer {
+ out customers(csDB:Map, addCustomer(uid:Str, org:Str)) = insert(csDB, uid, {"organization": org})
+}
+
+channel AddCampany {
+ out companies(cmDB:Map, addCampany(cid:Str, address:Str)) = insert(cmDB, cid, {"address": address})
+}
+
+channel SetCustomerOrganization(uid:Str) {
+ out customers.{uid}.organization(prevCid:Str, setOrganization(cid)) = cid
+}
+
+channel SetCompanyAddress(cid:Str) {
+ out companies.{cid}.address(prevAdd:Str, setAddress(add)) = add
+}
+
+channel UpdateCustomerAddress(uid:Str) {
+ in customers.{uid}.organization(prevCid, updateCustomerAddress(cid, add)) = cid
+ in companies.{cid}.address(prevAdd, updateCustomerAddress(cid, add)) = add
+ out customers.{uid}.address(prevAdd, updateCustomerAddress(cid, add)) = add
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model b/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model
deleted file mode 100644
index f140bff..0000000
--- a/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model
+++ /dev/null
@@ -1,33 +0,0 @@
-channel C_CustomerAOff_In {
- 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
-}
-
-channel C_CompanyC1Add_In {
- 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
-}
-
-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))
-}
-
-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))
-}
diff --git a/AlgebraicDataflowArchitectureModel/models/DataStore.model b/AlgebraicDataflowArchitectureModel/models/DataStore.model
new file mode 100644
index 0000000..9369d6a
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/DataStore.model
@@ -0,0 +1,22 @@
+channel AddCompany {
+ out companies(comps: Map, addComp(compId: Str, compName: Str, compAdd: Str))
+ = insert(comps, compId, {"name": compName, "address": compAdd})
+}
+
+channel AddCustomer {
+ out customers(custs: Map, addCust(custId: Str, custName: Str, cumpId: Str))
+ = insert(custs, custId, {"name": custName, "company": cumpId})
+}
+
+channel SendCompName(custId: Str) {
+ in customers.{custId}.company(curCompId: Str, sendCompName(compId: Str, compName: Str)) = compId
+ in companies.{compId}.name(curName: Str, sendCompName(compId: Str, compName: Str)) = compName
+ out customers.{custId}.companyName(curName: Str, sendCompName(compId, compName)) = compName
+}
+
+channel SendCompAddress(custId: Str) {
+ in customers.{custId}.company(curCompId: Str, sendCompAddress(compId: Str, compName: Str)) = compId
+ in companies.{compId}.address(curName: Str, sendCompAddress(compId: Str, compName: Str)) = compName
+ out customers.{custId}.companyAddress(curName: Str, sendCompAddress(compId, compName)) = compName
+}
+
diff --git a/AlgebraicDataflowArchitectureModel/models/DatabaseTest.model b/AlgebraicDataflowArchitectureModel/models/DatabaseTest.model
new file mode 100644
index 0000000..0ba12a5
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/DatabaseTest.model
@@ -0,0 +1,15 @@
+channel LoadDatabase {
+ out database(dbs: Map, load(url: Str, user: Str, pass: Str)) = insert(dbs, url, {"user": user, "password": pass, "query": "", "result": ""})
+}
+
+channel executeQuery(url: Str) {
+ out database.{url}.query(query: Str, execute(newQuery)) = newQuery
+}
+
+native channel sendQuery(url: Str) {
+ in database.{url}.query(query: Str, sendQuery(newQuery)) = newQuery
+}
+
+native channel setResult(url: Str) {
+ out database.{url}.result(resutlt: Str, setResult(newResult: Str)) = newResult
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/DatabaseTest2.model b/AlgebraicDataflowArchitectureModel/models/DatabaseTest2.model
new file mode 100644
index 0000000..4bb93e0
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/DatabaseTest2.model
@@ -0,0 +1,44 @@
+init {
+ db := {
+ "accountAndBooks": {
+ "url": "jdbc:postgresql://localhost:5432/postgres",
+ "user": "root",
+ "password": "pass",
+ "tables": {
+ "accounts": {
+ "record": nil
+ },
+ "books": {
+ "record": nil
+ }
+ }
+ }
+ }
+
+ current:= {
+ "aid": {
+ "value": 0,
+ "dbName": "accountAndBooks",
+ "table": "accounts",
+ "key": "aid"
+ },
+ "bid": {
+ "value": 0,
+ "dbName": "accountAndBooks",
+ "table": "books",
+ "key": "bid"
+ }
+ }
+}
+
+native channel setRecord(dbName: Str, tableName: Str) {
+ out db.{dbName}.tables.{tableName}.record(curRecord, setRecord(newRecord)) = newRecord
+}
+
+native channel updateRecordOnChangeCurrent(varName: Str) {
+ in current.{varName}.value(currentData, updateRecord(newCurrentData)) = newCurrentData
+}
+
+channel updateCurrent(varName: Str) {
+ out current.{varName}.value(curValue: Int, setValue(newValue: Int)) = newValue
+}
\ No newline at end of file
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/GroupChat.model b/AlgebraicDataflowArchitectureModel/models/GroupChat.model
new file mode 100644
index 0000000..1203e1a
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/GroupChat.model
@@ -0,0 +1,27 @@
+channel Signup {
+ out accounts(acDB:Map, signUp(aid:Str)) = insert(acDB, aid, {"notifications": nil})
+}
+
+channel HasRead(aid:Str) {
+ out accounts.{aid}.notifications(ntMap:Map, hasRead(gid:Str)) = delete(ntMap, gid)
+}
+
+channel CreateGroup {
+ out groups(grDB:Map, createGroup(gid:Str)) = insert(grDB, gid, {"members": nil, "messages": nil})
+}
+
+channel AddGroupMember(gid:Str) {
+ out groups.{gid}.members(memList:List, addGroupMember(aid:Str)) = append(memList, aid)
+}
+
+channel PostMessage(gid:Str) {
+ out groups.{gid}.messages(mesList:List, postMessage(message:Str)) = append(mesList, message)
+}
+
+channel Notify(gid:Str) {
+ in groups.{gid}.messages(prevMesList, notify(m)) = mesList
+ for EachMember(mno:Int) {
+ ref groups.{gid}.members.{mno}(m.{mno}:Str, notify(m))
+ out accounts.{m.{mno}:Str}.notifications(prevNtMap:Map, notify(m)) = insert(prevNtMap, gid, true)
+ }
+}
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/InventoryManagement.model b/AlgebraicDataflowArchitectureModel/models/InventoryManagement.model
new file mode 100644
index 0000000..578d56c
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/InventoryManagement.model
@@ -0,0 +1,7 @@
+channel ItemRegistration {
+ out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
+}
+
+channel ReceivingOrShipping(itemId:Str) {
+ out inventory.{itemId}.count(prev_quantity:Int, receiveOrShip(quantity:Int)) = prev_quantity + quantity
+}
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/Kinematics.model b/AlgebraicDataflowArchitectureModel/models/Kinematics.model
new file mode 100644
index 0000000..3d10af4
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Kinematics.model
@@ -0,0 +1,20 @@
+channel CIO {
+ 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
+}
+
+channel C2 {
+ 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
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/Kinetics.model b/AlgebraicDataflowArchitectureModel/models/Kinetics.model
deleted file mode 100644
index 5218206..0000000
--- a/AlgebraicDataflowArchitectureModel/models/Kinetics.model
+++ /dev/null
@@ -1,20 +0,0 @@
-channel CIO {
- 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
-}
-
-channel C2 {
- 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
-}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/NemophilaAccounts.model b/AlgebraicDataflowArchitectureModel/models/NemophilaAccounts.model
new file mode 100644
index 0000000..0158d26
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/NemophilaAccounts.model
@@ -0,0 +1,86 @@
+channel CIO_CreateAccount {
+ out accounts(acList:List, createAccount(name:Str)) = append(acList, {
+ "name": name,
+ "posts": nil,
+ "newFriend": null,
+ "delReqFriend": null,
+ "newRequesting": null,
+ "friends": nil,
+ "requesting": nil,
+ "requested": nil,
+ })
+}
+
+channel CIO_ChangeName(uid:Str) {
+ out accounts.{uid}.name(prevName:Str, changeName(name)) = name
+}
+
+channel CIO_CreatePost(uid:Str) {
+ out accounts.{uid}.posts(postsList:List, createPost(comment:Str)) = cons(comment:Str, postsList)
+}
+
+channel CIO_DeletePost(uid:Str) {
+ out accounts.{uid}.posts(postsList:List, deletePost(pid:Str)) = remove(postsList, pid:Str)
+}
+
+channel CIO_PostRequesting(sendId:Str) {
+ out accounts.{sendId}.newRequesting(preNewResuesting:Str, postRequesting(recvId:Str)) = recvId
+}
+
+channel C_AddRequesting(sendId:Str) {
+ in accounts.{sendId}.newRequesting(preNewResuesting:Str, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map)) = recvId
+ ref accounts.{sendId}.friends(sendFriends:Map, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map))
+ ref accounts.{sendId}.requested(sendRequested:Map, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map))
+ ref accounts.{recvId}.requesting(recvRequesting:Map, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map))
+
+ out accounts.{sendId}.requesting(sendRequesting:Map, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map)) = if(contains(sendFriends:Map, recvId) == true,
+ sendRequesting,
+ insert(sendRequesting:Map, recvId:Str, true))
+ out accounts.{recvId}.requested(recvRequested:Map, sync1(recvId:Str, sendRequested:Map, recvRequesting:Map, sendFriends:Map)) = if(contains(sendFriends:Map, recvId) == true,
+ recvRequested,
+ insert(recvRequested:Map, sendId:Str, true))
+}
+
+channel CIO_RejectRequest(recvId:Str) {
+ out accounts.{sendId}.requesting(sendRequesting:Map, rejectRequest(sendId:Str)) = delete(sendRequesting:Map, recvId:Str)
+ out accounts.{recvId}.requested(recvRequested:Map, rejectRequest(sendId:Str)) = delete(recvRequested:Map, sendId:Str)
+}
+
+channel CIO_AdmitFriend(recvId:Str) {
+ out accounts.{recvId}.newFriend(preNewFriend:Str, admitFriend(sendId:Str)) = sendId
+}
+
+channel C_AddFriend(recvId:Str) {
+ in accounts.{recvId}.newFriend(preSendId:Str, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map)) = sendId
+ ref accounts.{sendId}.requesting(preSendTing:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map))
+ ref accounts.{recvId}.requested(preRecvTed:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map))
+
+ out accounts.{sendId}.friends(sendFriends:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map)) = if(contains(preSendTing:Map, recvId) == true && contains(preRecvTed:Map, sendId) == true,
+ insert(sendFriends, recvId:Str, true),
+ sendFriends)
+ out accounts.{recvId}.friends(recvFriends:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map)) = if(contains(preSendTing:Map, recvId) == true && contains(preRecvTed:Map, sendId) == true,
+ insert(recvFriends, sendId:Str, true),
+ recvFriends)
+ out accounts.{sendId}.requesting(sendRequesting:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map)) = if(contains(preSendTing:Map, recvId) == true && contains(preRecvTed:Map, sendId) == true,
+ delete(sendRequesting:Map, recvId:Str),
+ sendRequesting)
+ out accounts.{recvId}.requested(recvRequested:Map, sync2(sendId:Str, preSendTing:Map, preRecvTed:Map)) = if(contains(preSendTing:Map, recvId) == true && contains(preRecvTed:Map, sendId) == true,
+ delete(recvRequested:Map, sendId:Str),
+ recvRequested)
+}
+
+channel CIO_DeleteFriendRequest(sendId:Str) {
+ out accounts.{sendId}.delReqFriend(preDelReqFriend:Str, deleteFriend(recvId:Str)) = recvId
+}
+
+channel CIO_DeleteFriend(sendId:Str) {
+ in accounts.{sendId}.delReqFriend(preRecvId:Str, sync3(recvId:Str, preSendFriends:Map, preRecvFriends:Map)) = recvId
+ ref accounts.{sendId}.friends(preSendFriends:Map, sync3(recvId:Str, preSendFriends:Map, preRecvFriends:Map))
+ ref accounts.{recvId}.friends(preRecvFriends:Map, sync3(recvId:Str, preSendFriends:Map, preRecvFriends:Map))
+ out accounts.{sendId}.friends(sendFriends:Map, sync3(recvId:Str, preSendFriends:Map, preRecvFriends:Map)) = if(contains(preSendFriends:Map, recvId) == true || contains(preRecvFriends:Map, sendId) == true,
+ delete(sendFriends:Map, recvId:Str),
+ sendFriends)
+ out accounts.{recvId}.friends(recvFriends:Map, sync3(recvId:Str, preSendFriends:Map, preRecvFriends:Map)) = if(contains(preSendFriends:Map, recvId) == true || contains(preRecvFriends:Map, sendId) == true,
+ delete(recvFriends:Map, sendId:Str),
+ recvFriends)
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame.model b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame.model
new file mode 100644
index 0000000..d91b144
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame.model
@@ -0,0 +1,31 @@
+channel Signup {
+ out accounts(acDB:Map, signUp(aid:Str, name:Str)) = insert(acDB, aid, {"name": name})
+}
+
+channel ChangeName(aid:Str) {
+ out accounts.{aid}.name(prevName:Str, changeName(name)) = name
+}
+
+channel CreateRoom {
+ out rooms(rmDB:Map, createRoom(rid:Str, blueId:Str, redId:Str)) = insert(rmDB, rid, {"blue_id": blueId, "red_id": redId})
+}
+
+channel ChangeRedId(rid:Str) {
+ out rooms.{rid}.red_id(prevRedId:Str, changeRedId(redId)) = redId
+}
+
+channel ChangeBlueId(rid:Str) {
+ out rooms.{rid}.blue_id(prevBlueId:Str, changeBlueId(blueId)) = blueId
+}
+
+channel UpdateRedName(rid:Str) {
+ in rooms.{rid}.red_id(prevAid:Str, updateRedName(aid, name)) = aid
+ in accounts.{aid}.name(prevName:Str, updateRedName(aid, name)) = name
+ out rooms.{rid}.red_name(prevName:Str, updateRedName(aid, name)) = name
+}
+
+channel UpdateBlueName(rid:Str) {
+ in rooms.{rid}.blue_id(prevAid:Str, updateBlueName(aid, name)) = aid
+ in accounts.{aid}.name(prevName:Str, updateBlueName(aid, name)) = name
+ out rooms.{rid}.blue_name(prevName:Str, updateBlueName(aid, name)) = name
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model
new file mode 100644
index 0000000..ccd15a7
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/OnlineBattleGame2.model
@@ -0,0 +1,33 @@
+channel Signup {
+ out accounts(acDB:Map, signUp(aid:Str, name:Str)) = insert(acDB, aid, {"name": name, "point": 0})
+}
+
+channel ChangeName(aid:Str) {
+ out accounts.{aid}.name(prevName:Str, changeName(name)) = name
+}
+
+channel CreateRoom {
+ out rooms(rmDB:Map, createRoom(rid:Str)) = insert(rmDB, rid, {"members": nil, "battle": false})
+}
+
+channel AddRoomMember(rid:Str) {
+ out rooms.{rid}.members(mList:List, addRoomMember(id:Str)) = append(mList, {"id": id})
+}
+
+channel Battle(rid:Str) {
+ out rooms.{rid}.battle(prevHasWon, battle(hasWon:Bool)) = hasWon
+}
+
+channel UpdateName(rid:Str, mno:Int) {
+ in rooms.{rid}.members.{mno}.id(prevMid:Str, updateName(mid, name)) = mid
+ in accounts.{mid}.name(prevName:Str, updateName(mid, name)) = name
+ out rooms.{rid}.members.{mno}.name(prevName:Str, updateName(mid, name)) = name
+}
+
+channel UpdatePoint(rid:Str) {
+ in rooms.{rid}.battle(prevState, updatePoint(hasWon, mid)) = hasWon
+ for EachMember(mno:Int) {
+ ref rooms.{rid}.members.{mno}.id(mid:Str, updatePoint(hasWon, mid))
+ out accounts.{mid}.point(prevPoint:Int, updatePoint(hasWon, mid)) = if(hasWon, prevPoint + 1, prevPoint)
+ }
+}
\ 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/RefBug.model b/AlgebraicDataflowArchitectureModel/models/RefBug.model
new file mode 100644
index 0000000..e421f6b
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/RefBug.model
@@ -0,0 +1,19 @@
+init {
+ constant := 10
+ variable := 10
+ ans := 20
+}
+
+channel changeVar {
+ out variable(cur: Int, change(next: Int)) = next
+}
+
+channel changeConst {
+ out constant(const: Int, change(next: Int)) = next
+}
+
+channel calcAns {
+ in variable(curVar: Int, calc(const: Int, nextVar: Int)) = nextVar
+ ref constant(const: Int, calc(const: Int, var: Int))
+ out ans(curAns: Int, calc(const: Int, var: Int)) = var + const
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/RestTest.model b/AlgebraicDataflowArchitectureModel/models/RestTest.model
new file mode 100644
index 0000000..2eb1271
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/RestTest.model
@@ -0,0 +1,40 @@
+native channel setResponse(num: Int) {
+ out restClients.{num}.response(prev: Str, setResponse(response)) = response
+}
+
+native channel changeState(num: Int) {
+ in restClients.{num}.state(state: Int, changeState(newState: Int)) = newState
+}
+
+
+channel creatClient{
+ out restClients(clients: List, create(url:Str, method:Str)) = append(clients, {
+ "url": url,
+ "method": method,
+ "body": nil,
+ "response": "",
+ "header": nil,
+ "state": 0
+ })
+}
+
+channel onResponse(num: Int) {
+ in restClients.{num}.response(res: Str, changeRes(newRes)) = newRes
+ out restClients.{num}.state(state: Int, changeRes(newRes)) = 0
+}
+
+channel setUrl(num: Int) {
+ out restClients.{num}.url(curUrl: Str, setUrl(newUrl)) = newUrl
+}
+
+channel addBody(num: Int) {
+ out restClients.{num}.body(body: Map, addBody(key: Str, value: Str)) = insert(body, key, value)
+}
+
+channel addHeader(num: Int) {
+ out restClients.{num}.header(header: Map, addHeader(key: Str, value: Str)) = insert(header, key, value)
+}
+
+channel setState(num: Int) {
+ out restClients.{num}.state(nowState: Int, setState(newState)) = newState
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/Search.model b/AlgebraicDataflowArchitectureModel/models/Search.model
new file mode 100644
index 0000000..e401c34
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Search.model
@@ -0,0 +1,25 @@
+init {
+ accounts := {"001": {"name": "Alice", "age": 25, "address": "Kobe"},
+ "002": {"name": "Bob", "age": 25, "address": "Osaka"},
+ "003": {"name": "Carol", "age": 22, "address": "Kobe"},
+ "004": {"name": "Dave", "age": 25, "address": "Kobe"}
+ }
+}
+
+channel Signup {
+ out accounts(acDB:Map, signUp(aid:Str, name:Str, age:Int, address:Str)) = insert(acDB, aid, {"name": name, "age": age, "address": address})
+}
+
+channel ChangeName(aid:Str) {
+ out accounts.{aid}.name(n:Str, changeName(name:Str)) = name
+}
+
+channel Query {
+ out query(q:Json, enterQuery(age:Int, address:Str)) = {"age": age, "address": address}
+}
+
+channel SearchAccount {
+ in accounts(acDB:Map, searchAccount(acDB2, q2)) = acDB2
+ in query(q:Json, searchAccount(acDB2, q2)) = q2
+ out result(resultMap:Map, searchAccount(acDB2, q2)) = search(acDB2, q2)
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleAddressBook.model b/AlgebraicDataflowArchitectureModel/models/SimpleAddressBook.model
new file mode 100644
index 0000000..9a9f38a
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleAddressBook.model
@@ -0,0 +1,11 @@
+channel Init {
+ out book.owner(pre_name: Str, init(name: Str)) = name
+}
+
+channel Add {
+ out book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr)
+}
+
+channel Del {
+ out book.addr(pre_addr: Map, del(name: Str)) = delete(pre_addr, name)
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleTwitter.model b/AlgebraicDataflowArchitectureModel/models/SimpleTwitter.model
new file mode 100644
index 0000000..486fafb
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleTwitter.model
@@ -0,0 +1,7 @@
+channel Signup {
+ out accounts(accountDB:Map, signUp(accountId:Str, name:Str)) = insert(accountDB, accountId, {"name": name, "tweets": nil})
+}
+
+channel Tweet(accountId:Str) {
+ out accounts.{accountId}.tweets(tweetList:List, tweet(contents:Str)) = append(tweetList, contents)
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleUI.model b/AlgebraicDataflowArchitectureModel/models/SimpleUI.model
new file mode 100644
index 0000000..6d4cb43
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI.model
@@ -0,0 +1,112 @@
+init {
+ screenTemplates := {
+ "000": {"widgets": {"001": {"type": "textInput", "text": "", "state": 0, "visible": true},
+ "002": {"type": "button", "text": "Next", "state": 0, "visible": true}},
+ "layout": true},
+ "001": {"widgets": {"003": {"type": "label", "text": "label", "state": 0, "visible": true},
+ "004": {"type": "button", "text": "Back", "state": 0, "visible": true}},
+ "layout": true}
+ }
+}
+
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+channel EventHandler1(scId: Str, wid: Str) {
+ in screenTemplates.{scId="000"}.widgets.{wid="002"}.state(curState: Int, handleEvent1(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent1(nextState)) = if(nextState == 0, "001", curScId)
+}
+
+channel EventHandler2(scId: Str, wid: Str) {
+ in screenTemplates.{scId="001"}.widgets.{wid="004"}.state(curState: Int, handleEvent2(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent2(nextState)) = if(nextState == 0, "000", curScId)
+}
+
+channel ChangeLayout {
+ out screen.layout(curLayout: Bool, changeLayout(layout)) = layout
+}
+
+channel ChangeX(wid: Str) {
+ out screen.widgets.{wid}.x(curX: Int, changeX(x)) = x
+}
+
+channel ChangeY(wid: Str) {
+ out screen.widgets.{wid}.y(curY: Int, changeY(y)) = y
+}
+
+channel AddButton {
+ out screen.widgets(widgets: Map, addButton(wid: Str, text: Str)) = insert(widgets, wid, {"type": "button", "text": text, "state": 0})
+}
+
+channel AddLabel {
+ out screen.widgets(widgets: Map, addLabel(wid: Str, text: Str)) = insert(widgets, wid, {"type": "label", "text": text, "state": 0})
+}
+
+channel AddTextInput {
+ out screen.widgets(widgets: Map, addTextInput(wid: Str)) = insert(widgets, wid, {"type": "textInput", "text": "", "state": 0})
+}
+
+channel AddMovableButton {
+ out screen.widgets(widgets: Map, addMovableButton(wid: Str, text: Str, x: Int, y: Int, width: Int, height: Int)) = insert(widgets, wid, {"type": "button", "text": text, "x": x, "y": y, "width": width, "height": height, "state": 0})
+}
+
+channel AddMovableLabel {
+ out screen.widgets(widgets: Map, addMovableLabel(wid: Str, text: Str, x: Int, y: Int, width: Int, height: Int)) = insert(widgets, wid, {"type": "label", "text": text, "x": x, "y": y, "width": width, "height": height, "state": 0})
+}
+
+channel AddMovableTextInput {
+ out screen.widgets(widgets: Map, addMovableTextInput(wid: Str, x: Int, y: Int, width: Int, height: Int)) = insert(widgets, wid, {"type": "textInput", "text": "", "x": x, "y": y, "width": width, "height": height, "state": 0})
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleUI2.model b/AlgebraicDataflowArchitectureModel/models/SimpleUI2.model
new file mode 100644
index 0000000..52bbcdd
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI2.model
@@ -0,0 +1,89 @@
+init {
+ screenTemplates := {
+ "000": {
+ "widgets": {
+ "001": {"type": "textInput", "visible": true},
+ "002": {"type": "button", "text": "Next", "visible": true},
+ "005": {"type": "label", "text": "", "visible": true},
+ "006": {"type": "button", "text": "hello", "visible": true}
+ },
+ "layout": true
+ },
+ "001": {
+ "widgets": {
+ "003": {"type": "label", "text": "label", "visible": true},
+ "004": {"type": "button", "text": "Back", "visible": true},
+ "007": {"type": "textInput", "visible": true}
+ },
+ "layout": true
+ }
+ }
+ sender5 := "005"
+}
+
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventHandler1(wid: Str) {
+ in screen.widgets.{wid="002"}.state(curState: Int, handleEvent1(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent1(nextState)) = if((curScId == "000") && (nextState == 0), "001", curScId)
+}
+
+channel EventHandler2(wid: Str) {
+ in screen.widgets.{wid="004"}.state(curState: Int, handleEvent2(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent2(nextState)) = if((curScId == "001") && (nextState == 0), "000", curScId)
+}
+
+channel EventHandler3(wid: Str) {
+ in screen.widgets.{wid="001"}.text(curText: Str, handler3(nextText: Str, target:Str)) = nextText
+ ref sender5(target, handler3(nextText, target))
+ out screen.widgets.{target}.text(curText, handler3(nextText, target)) = nextText
+}
+
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleUI3.model b/AlgebraicDataflowArchitectureModel/models/SimpleUI3.model
new file mode 100644
index 0000000..729c318
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI3.model
@@ -0,0 +1,142 @@
+init {
+ screenTemplates := {
+ "000": {
+ "widgets": {
+ "001": {"type": "label", "text": "aid", "state": 0, "visible": true},
+ "002": {"type": "textInput", "text": "", "state": 0, "visible": true},
+ "003": {"type": "label", "text": "name", "state": 0, "visible": true},
+ "004": {"type": "textInput", "text": "", "state": 0, "visible": true},
+ "005": {"type": "button", "text": "ok", "state": 0, "visible": true},
+ "006": {"type": "button", "text": "search", "state": 0, "visible": true}
+ },
+ "layout": true
+ },
+ "001" :{
+ "widgets": {
+ "101": {"type": "label", "text": "success!", "state": 0, "visible": true},
+ "102": {"type": "button", "text": "back", "state": 0, "visible": true}
+ },
+ "layout": true
+ },
+ "002": {
+ "widgets": {
+ "201": {"type": "textInput", "text": "", "state": 0, "visible": true},
+ "202": {"type": "label", "text": "aid", "state": 0, "visible": true},
+ "203": {"type": "label", "text": "", "state": 0, "visible": true}
+ }
+ },
+ "409": {
+ "widgets": {
+ "491": {"type": "label", "text": "conflilct!", "state": 0, "visible": true},
+ "492": {"type": "button", "text": "back", "state": 0, "visible": true}
+ },
+ "layout": true
+ }
+ }
+ sender1 := "002"
+ sender2 := "004"
+ sender3 := "203"
+}
+
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+channel EventDispatch2(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, dispatchEvent(curScId, wid, nextText)) = nextText
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextText))
+ out screenTemplates.{curScId}.widgets.{wid}.text(curText: Str, dispatchEvent(curScId, wid, nextText)) = nextText
+}
+
+channel addAccount {
+ out accounts(accounts, addAccounts(aid: Str, name: Str)) = insert(accounts, aid, name)
+}
+
+channel changeName(aid: Str) {
+ out accounts.{aid}.name(curName, changeName(nextName)) = nextName
+}
+
+channel EventHandler2(scId: Str, wid: Str) {
+ in screenTemplates.{scId="000"}.widgets.{wid="006"}.state(curState: Str, handleEvent(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent(nextState)) = if(nextState == 0, "002", curScId)
+}
+
+channel EventHandler3(scId: Str, wid: Str) {
+ in screenTemplates.{scId="000"}.widgets.{wid="005"}.state(curState: Str, handleEvent3(nextState, t1, t2, aid, name, accounts)) = nextState
+ ref sender1(t1, handleEvent3(nextState, t1, t2, aid, name, accounts))
+ ref sender2(t2, handleEvent3(nextState, t1, t2, aid, name, accounts))
+ ref screen.widgets.{t1}.text(aid, handleEvent3(nextState, t1, t2, aid, name, accounts))
+ ref screen.widgets.{t2}.text(name, handleEvent3(nextState, t1, t2, aid, name, accounts))
+ ref accounts(accounts, handleEvent3(nextState, t1, t2, aid, name, accounts))
+ out accounts(accounts, handleEvent3(nextState, t1, t2, aid, name, tmp)) = if(nextState==0, if(contains(accounts, aid), accounts, insert(accounts, aid, {"name": name})), accounts)
+ out curScreen(curScId: Str, handleEvent3(nextState, t1, t2, aid, name, accounts)) = if(nextState==0, if(contains(accounts, aid), "409", "001"), curScId)
+}
+
+channel EventHandler4(scId: Str, wid: Str) {
+ in screenTemplates.{scId="001"}.widgets.{wid="102"}.state(curState: Str, handleEvent4(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent4(nextState)) = if(nextState==0, "000", curScId)
+}
+
+channel EventHandler5(scId: Str, wid: Str) {
+ in screenTemplates.{scId="002"}.widgets.{wid="201"}.text(curText: Str, handleEvent5(nextText, target, accounts)) = nextText
+ ref sender3(target, handleEvent5(nextText, target, accounts))
+ ref accounts(accounts, handleEvent5(nextText, target, accounts))
+ out screen.widgets.{target}.text(curText, handleEvent5(nextText, target, accounts)) = if(containe(accounts, nextText), lookup(accounts, nextText), curText)
+}
+
+channel EventHandler5(scId: Str, wid: Str) {
+ in screenTemplates.{scId="409"}.widgets.{wid="492"}.state(curState: Str, handleEvent5(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent4(nextState)) = if(nextState==0, "000", curScId)
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleUI4.model b/AlgebraicDataflowArchitectureModel/models/SimpleUI4.model
new file mode 100644
index 0000000..c6be552
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI4.model
@@ -0,0 +1,118 @@
+init {
+ screenTemplates := {
+ "screen1":{
+ "widgets": {
+ "e6f7bcd0c6554748a87b74a3b39eea82": {"type": "button", "text": "button", "visible": true, "x": 175, "y": 200, "width": 100, "height": 40},
+ "f6af87118f8c4fa284a4a226f5369dd7": {"type": "label", "text": "label", "visible": true, "x": 99, "y": 23, "width": 100, "height": 40},
+ "idInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 94, "y": 64, "width": 100, "height": 40},
+ "nameInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 96, "y": 126, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen2":{
+ "widgets": {
+ "6ce2109a701e4883ac50f3f726ee1e47": {"type": "button", "text": "button", "visible": true, "x": 141, "y": 43, "width": 355, "height": 164}
+ },
+ "layout": false
+}
+ }
+ idInput := "idInput"
+ nameInput := "nameInput"
+}
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+channel EventDispatch2(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+ ref curScreen(curScId: Str, dispatchEvent2(curScId, wid, nextText))
+ out screenTemplates.{curScId}.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+}
+
+channel e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="e6f7bcd0c6554748a87b74a3b39eea82"}.state(curState, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef)) = nextState
+ ref idInput(idInput, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef))
+ ref screen.widgets.{idInput}.text(id, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef))
+ ref nameInput(nameInput, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef))
+ ref screen.widgets.{nameInput}.text(name, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef))
+ ref accounts(accountsRef, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef))
+ out accounts(accounts: Map, e6f7bcd0c6554748a87b74a3b39eea82AccountsSetData(nextState, id, idInput, name, nameInput, accountsRef)) = if((nextState == 0) && (id != "") && (!contains(accountsRef, id)), insert(accounts, id, {"name": name}), accounts)
+}
+
+channel addTweets {
+ out tweets(tweets: Map, addTweets(tid: Str, contents: Str, idOfAuthor: Str)) = insert(tweets, tid, {"contents": contents,"idOfAuthor": idOfAuthor})
+}
+
+channel changeContentsOfTweets(tid: Str) {
+ out tweets.{tid}.contents(contents: Str, changeContentsOfTweets(newContents: Str)) = newContents
+}
+
+channel changeIdOfAuthorOfTweets(tid: Str) {
+ out tweets.{tid}.idOfAuthor(idOfAuthor: Str, changeIdOfAuthorOfTweets(newIdOfAuthor: Str)) = newIdOfAuthor
+}
+
+channel nameOfAuthorOfTweets(tid: Str){
+ in tweets.{tid}.idOfAuthor(idOfAuthor: Str, nameOfAuthorOfTweets(newIdOfAuthor: Str, newNameOfAuthor: Str)) = newIdOfAuthor
+ in accounts.{newIdOfAuthor}.name(name: Str, nameOfAuthorOfTweets(newIdOfAuthor, newNameOfAuthor)) = newNameOfAuthor
+ out tweets.{tid}.nameOfAuthor(nameOfAuthor, nameOfAuthorOfTweets(newIdOfAuthor, newNameOfAuthor)) = newNameOfAuthor
+}
+
+channel addAccounts {
+ out accounts(accounts: Map, addAccounts(id: Str, name: Str)) = insert(accounts, id, {"name": name})
+}
+
+channel changeNameOfAccounts(id: Str) {
+ out accounts.{id}.name(name: Str, changeNameOfAccounts(newName: Str)) = newName
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/SimpleUI5.model b/AlgebraicDataflowArchitectureModel/models/SimpleUI5.model
new file mode 100644
index 0000000..7d6f424
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI5.model
@@ -0,0 +1,124 @@
+init {
+ screenTemplates := {
+ "screen1":{
+ "widgets": {
+ "btn1": {"type": "button", "text": "hello", "visible": true, "x": 10, "y": 10, "width": 100, "height": 40}
+ },
+ "layout": false
+}
+ }
+ curScreen := "screen1"
+ input1 := "input1"
+ input2 := "input2"
+ input3 := "input3"
+}
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+channel EventDispatch2(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+ ref curScreen(curScId: Str, dispatchEvent2(curScId, wid, nextText))
+ out screenTemplates.{curScId}.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+}
+
+channel btn1AccountsSetData(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="btn1"}.state(curState, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef)) = nextState
+ ref input1(input1, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref screen.widgets.{input1}.text(id, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref input2(input2, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref screen.widgets.{input2}.text(name, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref input3(input3, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref screen.widgets.{input3}.text(age, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ ref accounts(accountsRef, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef))
+ out accounts(accounts: Map, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef)) = if((nextState == 0) && (id != "") && (!contains(accountsRef, id)), insert(accounts, id, {"name": name, "age": age}), accounts)
+ out curScreen(curScreen, btn1AccountsSetData(nextState, id, input1, name, input2, age, input3, accountsRef)) = if((nextState == 0), if((id != "") && (!contains(accountsRef, id)), "screen2", "screen3"), curScreen)
+}
+
+channel addAccounts {
+ out accounts(accounts: Map, addAccounts(id: Str, name: Str, age: Int)) = insert(accounts, id, {"name": name,"age": age})
+}
+
+channel changeNameOfAccounts(id: Str) {
+ out accounts.{id}.name(name: Str, changeNameOfAccounts(newName: Str)) = newName
+}
+
+channel changeAgeOfAccounts(id: Str) {
+ out accounts.{id}.age(age: Int, changeAgeOfAccounts(newAge: Int)) = newAge
+}
+
+channel addTweets {
+ out tweets(tweets: Map, addTweets(tweetId: Int, contents: Str, idOfAccounts: Str)) = insert(tweets, tweetId, {"contents": contents,"idOfAccounts": idOfAccounts})
+}
+
+channel changeContentsOfTweets(tweetId: Int) {
+ out tweets.{tweetId}.contents(contents: Str, changeContentsOfTweets(newContents: Str)) = newContents
+}
+
+channel changeIdOfAccountsOfTweets(tweetId: Int) {
+ out tweets.{tweetId}.idOfAccounts(idOfAccounts: Str, changeIdOfAccountsOfTweets(newIdOfAccounts: Str)) = newIdOfAccounts
+}
+
+channel nameOfAccountsOfTweets(tweetId: Int){
+ in tweets.{tweetId}.idOfAccounts(idOfAccounts: Str, nameOfAccountsOfTweets(newIdOfAccounts: Str, newNameOfAccounts: Str)) = newIdOfAccounts
+ in accounts.{newIdOfAccounts}.name(name: Str, nameOfAccountsOfTweets(newIdOfAccounts, newNameOfAccounts)) = newNameOfAccounts
+ out tweets.{tweetId}.nameOfAccounts(nameOfAccounts, nameOfAccountsOfTweets(newIdOfAccounts, newNameOfAccounts)) = newNameOfAccounts
+}
+
+channel ageOfAccountsOfTweets(tweetId: Int){
+ in tweets.{tweetId}.idOfAccounts(idOfAccounts: Str, ageOfAccountsOfTweets(newIdOfAccounts: Str, newAgeOfAccounts: Int)) = newIdOfAccounts
+ in accounts.{newIdOfAccounts}.age(age: Int, ageOfAccountsOfTweets(newIdOfAccounts, newAgeOfAccounts)) = newAgeOfAccounts
+ out tweets.{tweetId}.ageOfAccounts(ageOfAccounts, ageOfAccountsOfTweets(newIdOfAccounts, newAgeOfAccounts)) = newAgeOfAccounts
+}
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
index 6ee866a..36d6966 100644
--- a/AlgebraicDataflowArchitectureModel/models/StockManagement2.model
+++ b/AlgebraicDataflowArchitectureModel/models/StockManagement2.model
@@ -4,10 +4,10 @@
}
channel CIO_enter {
- out deriver(s:Tuple, arrive(item:Str, num:Int)) == tuple(item, num, num)
+ 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)))
+ in deriver(dr, update3(dr2)) = dr2
+ out shipping(sp:Tuple, update3(dr2)) = tuple(fst(dr2), fst(snd(dr2)))
}
diff --git a/AlgebraicDataflowArchitectureModel/models/TableUI.model b/AlgebraicDataflowArchitectureModel/models/TableUI.model
new file mode 100644
index 0000000..defb520
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/TableUI.model
@@ -0,0 +1,114 @@
+init {
+ screenTemplates := {
+ "000": {
+ "widgets": {
+ "001": {"type": "textInput", "text": "", "state": 0, "visible": true},
+ "002": {"type": "table", "text": "testTeble", "state": 0, "visible": true,
+ "data": {"_": {"name": "_", "age": 0}},
+ "rowHeight": 40,
+ "colWidth": 100,
+ "columns": append(append(nil, "name"), "age"),
+ "primaryKeyName": "id",
+ }
+ },
+ "layout": true
+ }
+ }
+ screen1 := "000"
+ w002 := "002"
+}
+
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel OnTableChanged(wid: Str) {
+ in screen.widgets.{wid}.data(curData: Map, tableChanged(nextData)) = nextData
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+
+channel EventHandler1(scId: Str, wid: Str) {
+ in screenTemplates.{scId="000"}.widgets.{wid="002"}.state(curState: Int, handleEvent1(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent1(nextState)) = if(nextState == 0, "001", curScId)
+}
+
+channel EventHandler2(scId: Str, wid: Str) {
+ in screenTemplates.{scId="001"}.widgets.{wid="004"}.state(curState: Int, handleEvent2(nextState)) = nextState
+ out curScreen(curScId: Str, handleEvent2(nextState)) = if(nextState == 0, "000", curScId)
+}
+
+channel EventHandler3(curScId: Str, wid: Str) {
+ in screenTemplates.{curScId="000"}.widgets.{wid="002"}.data(curData: Map, handleEvent3(nextData, wid)) = nextData
+ out screen.widgets.{wid="002"}.data(curData: Map, handleEvent3(nextData, wid)) = nextData
+}
+
+channel addAccount {
+ out accounts(accounts: Map, addAccount(id: Str, name: Str, age: Int)) = insert(accounts, id, {"name": name, "age": age})
+}
+
+channel changeNameOfAccount(id: Str) {
+ out accounts.{id}.name(curName: Str, changeName(nextName: Str)) = nextName
+}
+
+channel changeNameOfAccount(id: Str) {
+ out accounts.{id}.age(curAge: Int, changeAge(nextAge: Int)) = nextAge
+}
+
+channel sendAccountToTable {
+ in accounts(cur: Map, sendAccount(next: Map, scId:Str, wid:Str)) = next
+ ref screen1(scId:Str, sendAccount(next, scId, wid))
+ ref w002(wid: Str, sendAccount(next, scId, wid))
+ out screenTemplates.{scId}.widgets.{wid}.data(cur: Map, sendAccount(next, scId, wid)) = next
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/Test.model b/AlgebraicDataflowArchitectureModel/models/Test.model
index a8a1348..70a16cd 100644
--- a/AlgebraicDataflowArchitectureModel/models/Test.model
+++ b/AlgebraicDataflowArchitectureModel/models/Test.model
@@ -1,9 +1,30 @@
-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
+init {
+ a := "001"
+ b := "hello"
+ c := {
+ "001": "ok",
+ "002": "bad"
+ }
+}
+
+channel add{
+ out b(cur: Str, add(next: Str)) = next
+}
+
+channel addC {
+ out c(cur: Map, addC(id: Str, name: Str)) = insert(cur, id, name)
+}
+
+channel changeC(id: Str) {
+ out c.{id}(cur: Str, changeC(next: Str)) = next
+}
+
+channel changeTarget {
+ out a(cur: Str, changeTarget(next: Str)) = next
+}
+
+channel send(id: Str) {
+ in b(cur: Str, send(next, target)) = next
+ ref a(target, send(next, target))
+ out c.{target}(cur: Str, send(next, target)) = next
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/TestTable.model b/AlgebraicDataflowArchitectureModel/models/TestTable.model
new file mode 100644
index 0000000..bef7ac2
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/TestTable.model
@@ -0,0 +1,309 @@
+init {
+ screenTemplates := {
+ "screen1":{
+ "widgets": {
+ "7019851523234447a240c3dedba971e5": {"type": "button", "text": "名刺登録", "visible": true, "x": 106, "y": 63, "width": 100, "height": 40},
+ "52d3cfc247dd4b44a880425d8121dd35": {"type": "button", "text": "名刺一覧", "visible": true, "x": 414, "y": 64, "width": 100, "height": 40},
+ "df8a46be90e541a29f236b8a1805dee3": {"type": "button", "text": "スタートアップ企業登録", "visible": true, "x": 55, "y": 197, "width": 197, "height": 41},
+ "730bd4998e06476c908909f5ea5d5214": {"type": "button", "text": "スタートアップ企業一覧", "visible": true, "x": 357, "y": 200, "width": 191, "height": 39}
+ },
+ "layout": false
+},
+ "screen2":{
+ "widgets": {
+ "eab4ab11006a4d4aad2941dc88e6c1c1": {"type": "label", "text": "住所", "visible": true, "x": 11, "y": 191, "width": 101, "height": 22},
+ "d91784537b284fe18600d341b0892205": {"type": "label", "text": "氏名", "visible": true, "x": 13, "y": 151, "width": 98, "height": 22},
+ "9e93ff73634f41a2b5140971719ef059": {"type": "label", "text": "会社名", "visible": true, "x": 14, "y": 101, "width": 104, "height": 28},
+ "393eb3ce387a4ae4ac3a37acbede16ec": {"type": "label", "text": "名刺id", "visible": true, "x": 10, "y": 58, "width": 98, "height": 21},
+ "7635b0b5c7d9473c83466ba17dfd4672": {"type": "label", "text": "名刺登録", "visible": true, "x": 254, "y": 14, "width": 100, "height": 40},
+ "compNameInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 107, "y": 104, "width": 386, "height": 26},
+ "addressInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 108, "y": 190, "width": 390, "height": 27},
+ "personNameInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 108, "y": 149, "width": 389, "height": 25},
+ "nameCardIdInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 107, "y": 58, "width": 392, "height": 26},
+ "7c349c606bda40bfa86f201d7ab07738": {"type": "button", "text": "戻る", "visible": true, "x": 94, "y": 263, "width": 100, "height": 40},
+ "4d368f3942014e34973c9573bc10f026": {"type": "button", "text": "登録", "visible": true, "x": 406, "y": 260, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen3":{
+ "widgets": {
+ "eb3f0d77a0e949e18ae46688fc08e4b8": {"type": "table", "text": "table", "visible": true, "x": 10, "y": 10, "width": 571, "height": 267, "data": {"_": {"companyName": "_", "personName": "_", "address": "_"}}, "columns": append(append(append(nil, "address"), "personName"), "companyName"), "primaryKeyName": "nameCardId"},
+ "9a7147d3c6a844cf91c748af4e8b975a": {"type": "button", "text": "戻る", "visible": true, "x": 244, "y": 285, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen4":{
+ "widgets": {
+ "56a620652f6849c1ac5646fde0bbab6e": {"type": "label", "text": "スタートアップid", "visible": true, "x": 5, "y": 54, "width": 106, "height": 23},
+ "1b6391c537be42e6b5781ae200f71df8": {"type": "label", "text": "代表者名", "visible": true, "x": 6, "y": 90, "width": 108, "height": 24},
+ "800ceeb6df24462fbed616c28a7d61a1": {"type": "label", "text": "代表者役職", "visible": true, "x": 6, "y": 126, "width": 99, "height": 21},
+ "b8f128ddd50041389ea1d72544ad5490": {"type": "label", "text": "名刺id", "visible": true, "x": 7, "y": 165, "width": 94, "height": 25},
+ "a971db3aa04b4387ba201ec5556385c7": {"type": "label", "text": "設立日", "visible": true, "x": 8, "y": 204, "width": 84, "height": 23},
+ "1bfed77c640141a493492c4c966ec7dc": {"type": "label", "text": "事業内容", "visible": true, "x": 7, "y": 243, "width": 88, "height": 27},
+ "45c778d316964c5d92c9211bee8220d6": {"type": "label", "text": "スタートアップ企業登録", "visible": true, "x": 205, "y": 11, "width": 172, "height": 29},
+ "startupIdInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 113, "y": 54, "width": 399, "height": 25},
+ "topNameInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 113, "y": 91, "width": 403, "height": 24},
+ "postInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 112, "y": 128, "width": 409, "height": 24},
+ "nameCardIdInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 112, "y": 165, "width": 408, "height": 27},
+ "establisedDateInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 112, "y": 204, "width": 416, "height": 24},
+ "contentsInput": {"type": "textInput", "text": "textInput", "visible": true, "x": 111, "y": 243, "width": 415, "height": 23},
+ "c34157984ccc4bf5b9d86f0ce366888f": {"type": "button", "text": "戻る", "visible": true, "x": 104, "y": 292, "width": 100, "height": 40},
+ "31737106f75b42829336630b7640cc59": {"type": "button", "text": "登録", "visible": true, "x": 406, "y": 289, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen5":{
+ "widgets": {
+ "42271e4903044634a535ba4a88f7c733": {"type": "table", "text": "table", "visible": true, "x": 6, "y": 8, "width": 569, "height": 274, "data": {"_": {"topName": "_", "topPost": "_", "companyNameOfCompany": "_", "addressOfCompany": "_", "establishedDate": "_", "contents": "_"}}, "columns": append(append(append(append(append(append(nil, "contents"), "establishedDate"), "addressOfCompany"), "companyNameOfCompany"), "topPost"), "topName"), "primaryKeyName": "startupCompanyId"},
+ "8314bfb998d24c26af0882c0d6bed852": {"type": "button", "text": "戻る", "visible": true, "x": 264, "y": 289, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen6":{
+ "widgets": {
+ "b0c9a7cd4ad54d529e2e9c82a7704d52": {"type": "label", "text": "登録に失敗しました", "visible": true, "x": 198, "y": 97, "width": 259, "height": 31},
+ "6f6349a4042a4604be8b3618da94eed8": {"type": "button", "text": "戻る", "visible": true, "x": 215, "y": 217, "width": 100, "height": 40}
+ },
+ "layout": false
+},
+ "screen7":{
+ "widgets": {
+ "c7d077fc04d64b11a6e8372fb7defee0": {"type": "button", "text": "button", "visible": true, "x": 10, "y": 10, "width": 100, "height": 40}
+ },
+ "layout": false
+}
+ }
+ curScreen := "screen1"
+ nameCardIdInput := "nameCardIdInput"
+ compNameInput := "compNameInput"
+ personNameInput := "personNameInput"
+ addressInput := "addressInput"
+ screen3 := "screen3"
+ eb3f0d77a0e949e18ae46688fc08e4b8 := "eb3f0d77a0e949e18ae46688fc08e4b8"
+ startupIdInput := "startupIdInput"
+ topNameInput := "topNameInput"
+ postInput := "postInput"
+ nameCardIdInput := "nameCardIdInput"
+ establisedDateInput := "establisedDateInput"
+ contentsInput := "contentsInput"
+ screen5 := "screen5"
+ 42271e4903044634a535ba4a88f7c733 := "42271e4903044634a535ba4a88f7c733"
+ nameCardIdInput := "nameCardIdInput"
+ compNameInput := "compNameInput"
+ personNameInput := "personNameInput"
+ addressInput := "addressInput"
+ startupIdInput := "startupIdInput"
+ topNameInput := "topNameInput"
+ postInput := "postInput"
+ nameCardIdInput := "nameCardIdInput"
+ establisedDateInput := "establisedDateInput"
+ contentsInput := "contentsInput"
+}
+native channel ScreenUpdate {
+ in screen(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel SetLayout {
+ in screen.layout(curLayout: Bool, setLayout(nextLayout)) = nextLayout
+}
+
+native channel SetVisible(wid: Str) {
+ in screen.widgets.{wid}.visible(curVisible: Bool, setVisible(nextVisible)) = nextVisible
+}
+
+native channel SetText(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, setText(nextText)) = nextText
+}
+
+native channel SetX(wid: Str) {
+ in screen.widgets.{wid}.x(curX: Int, setX(nextX)) = nextX
+}
+
+native channel SetY(wid: Str) {
+ in screen.widgets.{wid}.y(curY: Int, setY(nextY)) = nextY
+}
+
+native channel SetWidth(wid: Str) {
+ in screen.widgets.{wid}.width(curWidth: Int, setWidth(nextWidth)) = nextWidth
+}
+
+native channel SetHeight(wid: Str) {
+ in screen.widgets.{wid}.height(curHeight: Int, setHeight(nextHeight)) = nextHeight
+}
+
+native channel OnTableChanged(wid: Str) {
+ in screen.widgets.{wid}.data(curData: Map, tableChanged(nextData)) = nextData
+}
+
+native channel MouseEvent(wid: Str) {
+ out screen.widgets.{wid}.state(curState: Int, mouseEvent(nextState)) = nextState
+}
+
+native channel TextEvent(wid: Str) {
+ out screen.widgets.{wid}.text(curText: Str, textEvent(nextText)) = nextText
+}
+
+channel ChangeCurScreen {
+ out curScreen(curScId: Str, changeCurScreen(nextScId)) = nextScId
+}
+
+channel ScreenTransition {
+ in curScreen(curScId: Str, transScreen(nextScId, screen)) = nextScId
+ ref screenTemplates.{nextScId}(screen, transScreen(nextScId, screen))
+ out screen(curS, transScreen(nextScId, screen)) = screen
+}
+
+channel EventDispatch(wid: Str) {
+ in screen.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+ ref curScreen(curScId: Str, dispatchEvent(curScId, wid, nextState))
+ out screenTemplates.{curScId}.widgets.{wid}.state(curState: Int, dispatchEvent(curScId, wid, nextState)) = nextState
+}
+
+channel EventDispatch2(wid: Str) {
+ in screen.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+ ref curScreen(curScId: Str, dispatchEvent2(curScId, wid, nextText))
+ out screenTemplates.{curScId}.widgets.{wid}.text(curText: Str, dispatchEvent2(curScId, wid, nextText)) = nextText
+}
+
+channel OnWidgetUpdata(scId: Str, wid: Str) {
+ ref curScreen(curScId: Str, handle(curScId: Str, screen: Json, wid))
+ in screenTemplates.{scId=curScId}.widgets.{wid}(curScreen, handle(curScId, nextScreen, wid)) = nextScreen
+ out screen.widgets.{wid}(cur, handler(curScId, next, wid)) = next
+}
+
+channel 7019851523234447a240c3dedba971e5Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="7019851523234447a240c3dedba971e5"}.state(curState: Str, 7019851523234447a240c3dedba971e5Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 7019851523234447a240c3dedba971e5Navigate(nextState)) = if(nextState==0, "screen2", curScId)
+}
+channel 52d3cfc247dd4b44a880425d8121dd35Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="52d3cfc247dd4b44a880425d8121dd35"}.state(curState: Str, 52d3cfc247dd4b44a880425d8121dd35Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 52d3cfc247dd4b44a880425d8121dd35Navigate(nextState)) = if(nextState==0, "screen3", curScId)
+}
+channel df8a46be90e541a29f236b8a1805dee3Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="df8a46be90e541a29f236b8a1805dee3"}.state(curState: Str, df8a46be90e541a29f236b8a1805dee3Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, df8a46be90e541a29f236b8a1805dee3Navigate(nextState)) = if(nextState==0, "screen4", curScId)
+}
+channel 730bd4998e06476c908909f5ea5d5214Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen1"}.widgets.{wid="730bd4998e06476c908909f5ea5d5214"}.state(curState: Str, 730bd4998e06476c908909f5ea5d5214Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 730bd4998e06476c908909f5ea5d5214Navigate(nextState)) = if(nextState==0, "screen5", curScId)
+}
+channel 7c349c606bda40bfa86f201d7ab07738Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen2"}.widgets.{wid="7c349c606bda40bfa86f201d7ab07738"}.state(curState: Str, 7c349c606bda40bfa86f201d7ab07738Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 7c349c606bda40bfa86f201d7ab07738Navigate(nextState)) = if(nextState==0, "screen1", curScId)
+}
+channel 4d368f3942014e34973c9573bc10f026NameCardsSetData(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen2"}.widgets.{wid="4d368f3942014e34973c9573bc10f026"}.state(curState, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef)) = nextState
+ ref nameCardIdInput(nameCardIdInput, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref screen.widgets.{nameCardIdInput}.text(nameCardId, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref compNameInput(compNameInput, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref screen.widgets.{compNameInput}.text(companyName, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref personNameInput(personNameInput, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref screen.widgets.{personNameInput}.text(personName, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref addressInput(addressInput, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref screen.widgets.{addressInput}.text(address, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ ref nameCards(nameCardsRef, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef))
+ out nameCards(nameCards: Map, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef)) = if((nextState == 0) && (nameCardId != "") && (!contains(nameCardsRef, nameCardId)), insert(nameCards, nameCardId, {"companyName": companyName, "personName": personName, "address": address}), nameCards)
+ out curScreen(curScreen, 4d368f3942014e34973c9573bc10f026NameCardsSetData(nextState, nameCardId, nameCardIdInput, companyName, compNameInput, personName, personNameInput, address, addressInput, nameCardsRef)) = if((nextState == 0), if((nameCardId != "") && (!contains(nameCardsRef, nameCardId)), "screen1", "screen6"), curScreen)
+}
+channel sendNameCardsToEb3f0d77a0e949e18ae46688fc08e4b8 {
+ in nameCards(cur: Map, sendNameCardsToEb3f0d77a0e949e18ae46688fc08e4b8(next: Map, scId:Str, wid:Str)) = next
+ ref screen3(scId:Str, sendNameCardsToEb3f0d77a0e949e18ae46688fc08e4b8(next, scId, wid))
+ ref eb3f0d77a0e949e18ae46688fc08e4b8(wid: Str, sendNameCardsToEb3f0d77a0e949e18ae46688fc08e4b8(next, scId, wid))
+ out screenTemplates.{scId}.widgets.{wid}.data(cur: Map, sendNameCardsToEb3f0d77a0e949e18ae46688fc08e4b8(next, scId, wid)) = next
+}
+
+
+channel 9a7147d3c6a844cf91c748af4e8b975aNavigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen3"}.widgets.{wid="9a7147d3c6a844cf91c748af4e8b975a"}.state(curState: Str, 9a7147d3c6a844cf91c748af4e8b975aNavigate(nextState)) = nextState
+ out curScreen(curScId: Str, 9a7147d3c6a844cf91c748af4e8b975aNavigate(nextState)) = if(nextState==0, "screen1", curScId)
+}
+channel c34157984ccc4bf5b9d86f0ce366888fNavigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen4"}.widgets.{wid="c34157984ccc4bf5b9d86f0ce366888f"}.state(curState: Str, c34157984ccc4bf5b9d86f0ce366888fNavigate(nextState)) = nextState
+ out curScreen(curScId: Str, c34157984ccc4bf5b9d86f0ce366888fNavigate(nextState)) = if(nextState==0, "screen1", curScId)
+}
+channel 31737106f75b42829336630b7640cc59StartupCompanySetData(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen4"}.widgets.{wid="31737106f75b42829336630b7640cc59"}.state(curState, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef)) = nextState
+ ref startupIdInput(startupIdInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{startupIdInput}.text(startupCompanyId, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref topNameInput(topNameInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{topNameInput}.text(topName, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref postInput(postInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{postInput}.text(topPost, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref nameCardIdInput(nameCardIdInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{nameCardIdInput}.text(nameCardIdOfCompany, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref establisedDateInput(establisedDateInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{establisedDateInput}.text(establishedDate, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref contentsInput(contentsInput, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref screen.widgets.{contentsInput}.text(contents, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ ref startupCompany(startupCompanyRef, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef))
+ out startupCompany(startupCompany: Map, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef)) = if((nextState == 0) && (startupCompanyId != "") && (!contains(startupCompanyRef, startupCompanyId)), insert(startupCompany, startupCompanyId, {"topName": topName, "topPost": topPost, "nameCardIdOfCompany": nameCardIdOfCompany, "establishedDate": establishedDate, "contents": contents}), startupCompany)
+ out curScreen(curScreen, 31737106f75b42829336630b7640cc59StartupCompanySetData(nextState, startupCompanyId, startupIdInput, topName, topNameInput, topPost, postInput, nameCardIdOfCompany, nameCardIdInput, establishedDate, establisedDateInput, contents, contentsInput, startupCompanyRef)) = if((nextState == 0), if((startupCompanyId != "") && (!contains(startupCompanyRef, startupCompanyId)), "screen1", "screen6"), curScreen)
+}
+channel sendStartupCompanyTo42271e4903044634a535ba4a88f7c733 {
+ in startupCompany(cur: Map, sendStartupCompanyTo42271e4903044634a535ba4a88f7c733(next: Map, scId:Str, wid:Str)) = next
+ ref screen5(scId:Str, sendStartupCompanyTo42271e4903044634a535ba4a88f7c733(next, scId, wid))
+ ref 42271e4903044634a535ba4a88f7c733(wid: Str, sendStartupCompanyTo42271e4903044634a535ba4a88f7c733(next, scId, wid))
+ out screenTemplates.{scId}.widgets.{wid}.data(cur: Map, sendStartupCompanyTo42271e4903044634a535ba4a88f7c733(next, scId, wid)) = next
+}
+
+
+channel 8314bfb998d24c26af0882c0d6bed852Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen5"}.widgets.{wid="8314bfb998d24c26af0882c0d6bed852"}.state(curState: Str, 8314bfb998d24c26af0882c0d6bed852Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 8314bfb998d24c26af0882c0d6bed852Navigate(nextState)) = if(nextState==0, "screen1", curScId)
+}
+channel 6f6349a4042a4604be8b3618da94eed8Navigate(scId: Str, wid: Str){
+ in screenTemplates.{scId="screen6"}.widgets.{wid="6f6349a4042a4604be8b3618da94eed8"}.state(curState: Str, 6f6349a4042a4604be8b3618da94eed8Navigate(nextState)) = nextState
+ out curScreen(curScId: Str, 6f6349a4042a4604be8b3618da94eed8Navigate(nextState)) = if(nextState==0, "screen1", curScId)
+}
+
+channel addNameCards {
+ out nameCards(nameCards: Map, addNameCards(nameCardId: Str, companyName: Str, personName: Str, address: Str)) = insert(nameCards, nameCardId, {"companyName": companyName,"personName": personName,"address": address})
+}
+
+channel changeCompanyNameOfNameCards(nameCardId: Str) {
+ out nameCards.{nameCardId}.companyName(companyName: Str, changeCompanyNameOfNameCards(newCompanyName: Str)) = newCompanyName
+}
+
+channel changePersonNameOfNameCards(nameCardId: Str) {
+ out nameCards.{nameCardId}.personName(personName: Str, changePersonNameOfNameCards(newPersonName: Str)) = newPersonName
+}
+
+channel changeAddressOfNameCards(nameCardId: Str) {
+ out nameCards.{nameCardId}.address(address: Str, changeAddressOfNameCards(newAddress: Str)) = newAddress
+}
+
+channel addStartupCompany {
+ out startupCompany(startupCompany: Map, addStartupCompany(startupCompanyId: Str, topName: Str, topPost: Str, establishedDate: Str, contents: Str, nameCardIdOfCompany: Str)) = insert(startupCompany, startupCompanyId, {"topName": topName,"topPost": topPost,"establishedDate": establishedDate,"contents": contents,"nameCardIdOfCompany": nameCardIdOfCompany})
+}
+
+channel changeTopNameOfStartupCompany(startupCompanyId: Str) {
+ out startupCompany.{startupCompanyId}.topName(topName: Str, changeTopNameOfStartupCompany(newTopName: Str)) = newTopName
+}
+
+channel changeTopPostOfStartupCompany(startupCompanyId: Str) {
+ out startupCompany.{startupCompanyId}.topPost(topPost: Str, changeTopPostOfStartupCompany(newTopPost: Str)) = newTopPost
+}
+
+channel changeEstablishedDateOfStartupCompany(startupCompanyId: Str) {
+ out startupCompany.{startupCompanyId}.establishedDate(establishedDate: Str, changeEstablishedDateOfStartupCompany(newEstablishedDate: Str)) = newEstablishedDate
+}
+
+channel changeContentsOfStartupCompany(startupCompanyId: Str) {
+ out startupCompany.{startupCompanyId}.contents(contents: Str, changeContentsOfStartupCompany(newContents: Str)) = newContents
+}
+
+channel changeNameCardIdOfCompanyOfStartupCompany(startupCompanyId: Str) {
+ out startupCompany.{startupCompanyId}.nameCardIdOfCompany(nameCardIdOfCompany: Str, changeNameCardIdOfCompanyOfStartupCompany(newNameCardIdOfCompany: Str)) = newNameCardIdOfCompany
+}
+
+channel companyNameOfCompanyOfStartupCompany(startupCompanyId: Str){
+ in startupCompany.{startupCompanyId}.nameCardIdOfCompany(nameCardIdOfCompany: Str, companyNameOfCompanyOfStartupCompany(newNameCardIdOfCompany: Str, newCompanyNameOfCompany: Str)) = newNameCardIdOfCompany
+ in nameCards.{newNameCardIdOfCompany}.companyName(companyName: Str, companyNameOfCompanyOfStartupCompany(newNameCardIdOfCompany, newCompanyNameOfCompany)) = newCompanyNameOfCompany
+ out startupCompany.{startupCompanyId}.companyNameOfCompany(companyNameOfCompany, companyNameOfCompanyOfStartupCompany(newNameCardIdOfCompany, newCompanyNameOfCompany)) = newCompanyNameOfCompany
+}
+
+channel addressOfCompanyOfStartupCompany(startupCompanyId: Str){
+ in startupCompany.{startupCompanyId}.nameCardIdOfCompany(nameCardIdOfCompany: Str, addressOfCompanyOfStartupCompany(newNameCardIdOfCompany: Str, newAddressOfCompany: Str)) = newNameCardIdOfCompany
+ in nameCards.{newNameCardIdOfCompany}.address(address: Str, addressOfCompanyOfStartupCompany(newNameCardIdOfCompany, newAddressOfCompany)) = newAddressOfCompany
+ out startupCompany.{startupCompanyId}.addressOfCompany(addressOfCompany, addressOfCompanyOfStartupCompany(newNameCardIdOfCompany, newAddressOfCompany)) = newAddressOfCompany
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/Timer.model b/AlgebraicDataflowArchitectureModel/models/Timer.model
new file mode 100644
index 0000000..83a66d5
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Timer.model
@@ -0,0 +1,15 @@
+native channel TimersUpdated {
+ in timers(curTimers: Map, update(curTimers, nextTimers)) = nextTimers
+}
+
+native channel TimerEvent(tid: Str) {
+ out timers.{tid}.count(count: Long, tick()) = count + 1
+}
+
+channel StartTimer {
+ out timers(timers: Map, startTimer(tid: Str, interval: Long)) = insert(timers, tid, {"interval": interval, "count": 0})
+}
+
+channel ClearTimer {
+ out timers(timers: Map, clearTimer(tid: Str)) = delete(timers, tid)
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/TravelDistance.model b/AlgebraicDataflowArchitectureModel/models/TravelDistance.model
new file mode 100644
index 0000000..07d12db
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/TravelDistance.model
@@ -0,0 +1,13 @@
+channel CX {
+ 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
+}
+
+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)
+}
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..e5c46a8 100644
--- a/AlgebraicDataflowArchitectureModel/models/Twitter.model
+++ b/AlgebraicDataflowArchitectureModel/models/Twitter.model
@@ -1,47 +1,20 @@
-channel a_Tweet {
- out a_tweets(l:List, a_tweet(t:Str, time:Long)) == cons(tuple(time, t), l)
+channel SignUp {
+ out accounts(acDB:Map, signup(id:Str, name:Str)) = insert(acDB, id, {"name": name, "tweets": nil, "followees": nil, "timeline": nil})
}
-channel a_Follow {
- out a_following(f:List, a_follow(u:Int)) == cons(u, f)
+channel Tweet(id:Str) {
+ out accounts.{id}.tweets(twList:List, tweet(text:Str, time:Long)) = append(twList, {"time": time, "text": text})
}
-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)))
+channel AddFollowee(id:Str) {
+ out accounts.{id}.followees(fwList:List, addFollowee(flwId:Str)) = append(fwList, flwId)
}
-channel b_Tweet {
- 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)
-}
-
-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)))
-}
-
-channel c_Tweet {
- 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)
-}
-
-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)))
-}
+channel UpdateTimeline(myId:Str) {
+ in accounts.{myId}.tweets(t1:List, m) = m.myTweets
+ for EachFollowee(no:Int) {
+ in accounts.{myId}.followees.{no}(id:Str, m) = m.flw.{no}.id
+ in accounts.{m.flw.{no}.id}.tweets(t2:List, m) = m.flw.{no}.tweets
+ }
+ out accounts.{myId}.timeline(l:List, m) = merge(m.myTweets, m.flw)
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/VotingSystem.model b/AlgebraicDataflowArchitectureModel/models/VotingSystem.model
new file mode 100644
index 0000000..ff425db
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/VotingSystem.model
@@ -0,0 +1,14 @@
+channel Signup {
+ out accounts(acDB:Map, signUp(aid:Str, name:Str)) = insert(acDB, aid, {"name": name, "vote": null})
+}
+
+channel Cast(aid:Str) {
+ out accounts.{aid}.vote(preV, cast(v:Str)) = v
+}
+
+channel Collect {
+ for EachAccount(aid:Str) {
+ in accounts.{aid}.vote(preV:Str, collect(m)) = m.{aid}
+ }
+ out counts(preCnts:Json, collect(m)) = m
+}
\ No newline at end of file
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/prototypes/JAX-RS/Accounts/Account.java b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Accounts/Account.java
new file mode 100644
index 0000000..423e265
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Accounts/Account.java
@@ -0,0 +1,19 @@
+import java.util.*;
+
+public class Account {
+ private String name;
+ public Map getValue() {
+ Map temp_nil1 = new HashMap<>();
+ temp_nil1.put("name",this.getName());
+ return temp_nil1;
+ }
+ public String getName() {
+ return this.name;
+ }
+ public void changeName(int uid, String name) {
+ this.name = name;
+ }
+ public Account(String name) {
+ this.name = name;
+ }
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Accounts/Accounts.java b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Accounts/Accounts.java
new file mode 100644
index 0000000..d851471
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Accounts/Accounts.java
@@ -0,0 +1,42 @@
+import java.util.*;
+import javax.ws.rs.*;
+import javax.ws.rs.client.*;
+import javax.ws.rs.core.*;
+import org.springframework.stereotype.Component;
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.core.JsonProcessingException;
+
+@Path("/accounts")
+@Component
+public class Accounts {
+ private List value = new ArrayList<>();
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public List getValue() {
+ return new ArrayList<>(value);
+ }
+ public Account getAccount(int uid) {
+ return this.value.get(uid);
+ }
+ @Path("/{uid}")
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public Map getAccountValue(@PathParam("uid") int uid) {
+ return getAccount(uid).getValue();
+ }
+ @Path("/{uid}/name")
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public String getNameValue(@PathParam("uid") int uid) {
+ return getAccount(uid).getName();
+ }
+ @POST
+ public void signup(@FormParam("name") String name) {
+ this.value.add(new Account(name));
+ }
+ @Path("/{uid}/name")
+ @PUT
+ public void changeName(@PathParam("uid") int uid, @FormParam("name") String name) {
+ getAccount(uid).changeName(uid, name);
+ }
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour.java b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour.java
new file mode 100644
index 0000000..a7acf75
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour.java
@@ -0,0 +1,28 @@
+import java.util.*;
+import javax.ws.rs.*;
+import javax.ws.rs.client.*;
+import javax.ws.rs.core.*;
+import org.springframework.stereotype.Component;
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.core.JsonProcessingException;
+
+@Path("/hour")
+@Component
+public class Hour {
+ private int value = 0;
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public int getValue() {
+ return value;
+ }
+ @POST
+ public void updateFromMin(@FormParam("min") int min) {
+ int temp_if0;
+ if ((min==0)) {
+ temp_if0 = ((this.value+1)%24);
+ } else {
+ temp_if0 = this.value;
+ }
+ this.value = temp_if0;
+ }
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour_ang.java b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour_ang.java
new file mode 100644
index 0000000..9c14018
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Hour_ang.java
@@ -0,0 +1,19 @@
+import java.util.*;
+import javax.ws.rs.*;
+import javax.ws.rs.client.*;
+import javax.ws.rs.core.*;
+import org.springframework.stereotype.Component;
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.core.JsonProcessingException;
+
+@Path("/hour_ang")
+@Component
+public class Hour_ang {
+ private Client client = ClientBuilder.newClient();
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public double getValue() {
+ int hour = client.target("http://localhost:8080").path("/hour").request().get(int.class);
+ return ((hour/6)*Math.PI);
+ }
+}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Min.java b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Min.java
new file mode 100644
index 0000000..db4cea5
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/prototypes/JAX-RS/Clock/PULL-first/Min.java
@@ -0,0 +1,27 @@
+import java.util.*;
+import javax.ws.rs.*;
+import javax.ws.rs.client.*;
+import javax.ws.rs.core.*;
+import org.springframework.stereotype.Component;
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.core.JsonProcessingException;
+
+@Path("/min")
+@Component
+public class Min {
+ private int value = 0;
+ private Client client = ClientBuilder.newClient();
+ @Produces(MediaType.APPLICATION_JSON)
+ @GET
+ public int getValue() {
+ return value;
+ }
+ @POST
+ public void tick() throws JsonProcessingException {
+ Form form = new Form();
+ form.param("min", Integer.toString(this.value));
+ Entity