diff --git a/.idea/compiler.xml b/.idea/compiler.xml
new file mode 100644
index 0000000..fa782b8
--- /dev/null
+++ b/.idea/compiler.xml
@@ -0,0 +1,13 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/encodings.xml b/.idea/encodings.xml
new file mode 100644
index 0000000..bc9dc65
--- /dev/null
+++ b/.idea/encodings.xml
@@ -0,0 +1,7 @@
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/jarRepositories.xml b/.idea/jarRepositories.xml
new file mode 100644
index 0000000..712ab9d
--- /dev/null
+++ b/.idea/jarRepositories.xml
@@ -0,0 +1,20 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/misc.xml b/.idea/misc.xml
new file mode 100644
index 0000000..7816306
--- /dev/null
+++ b/.idea/misc.xml
@@ -0,0 +1,12 @@
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/modules.xml b/.idea/modules.xml
new file mode 100644
index 0000000..748a0cc
--- /dev/null
+++ b/.idea/modules.xml
@@ -0,0 +1,8 @@
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/vcs.xml b/.idea/vcs.xml
new file mode 100644
index 0000000..35eb1dd
--- /dev/null
+++ b/.idea/vcs.xml
@@ -0,0 +1,6 @@
+
+
+
+
+
+
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/.classpath b/AlgebraicDataflowArchitectureModel/.classpath
index 3e99697..9d5db7b 100644
--- a/AlgebraicDataflowArchitectureModel/.classpath
+++ b/AlgebraicDataflowArchitectureModel/.classpath
@@ -1,12 +1,13 @@
+
-
+
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/AlgebraicDataflowArchitectureModel.iml b/AlgebraicDataflowArchitectureModel/AlgebraicDataflowArchitectureModel.iml
new file mode 100644
index 0000000..0d73431
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/AlgebraicDataflowArchitectureModel.iml
@@ -0,0 +1,47 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/Accounts.model b/AlgebraicDataflowArchitectureModel/models/Accounts.model
new file mode 100644
index 0000000..24710ee
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/Accounts.model
@@ -0,0 +1,7 @@
+channel CIO1 {
+ out accounts(l:List, signup(name:Str)) = append(l, {"name": name})
+}
+
+channel CIO2(uid:Int) {
+ out accounts.{uid}.name(n:Str, changeName(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/Citrus.model b/AlgebraicDataflowArchitectureModel/models/Citrus.model
new file mode 100644
index 0000000..bcea2b2
--- /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))))
+}
\ No newline at end of file
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/CustomerOffice.model b/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model
index f140bff..5714436 100644
--- a/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model
+++ b/AlgebraicDataflowArchitectureModel/models/CustomerOffice.model
@@ -1,33 +1,21 @@
-channel C_CustomerAOff_In {
- out customerA_off(c:String, setOff(x)) == x
- out customerA_off(c, e) == c
+channel AddCustomer {
+ out customers(csDB:Map, addCustomer(uid:Str, office:Str)) = insert(csDB, uid, {"office": office})
}
-channel C_CustomerBOff_In {
- out customerB_off(c:String, setOff(x)) == x
- out customerB_off(c, e) == c
+channel AddCampany {
+ out companies(cmDB:Map, addCampany(cid:Str, address:Str)) = insert(cmDB, cid, {"address": address})
}
-channel C_CompanyC1Add_In {
- out companyC1_add(a:String, setAdd(y)) == y
- out companyC1_add(a, e) == a
+channel SetCustomerOffice(uid:Str) {
+ out customers.{uid}.office(prevCid:Str, setOffice(cid)) = cid
}
-channel C_CompanyC2Add_In {
- out companyC2_add(a:String, setAdd(y)) == y
- out companyC2_add(a, e) == a
+channel SetCompanyAddress(cid:Str) {
+ out companies.{cid}.address(prevAdd:Str, setAddress(add)) = add
}
-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))
+channel UpdateCustomerAddress(uid:Str) {
+ in customers.{uid}.office(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/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/GameEngine.model b/AlgebraicDataflowArchitectureModel/models/GameEngine.model
new file mode 100644
index 0000000..8c6f525
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/GameEngine.model
@@ -0,0 +1,104 @@
+init {
+ enemy := {
+ "position": {"x": 0.0, "y": 0.0, "z": 0.0},
+ "rotation": {"x": 0.0, "y": 0.0, "z": 0.0},
+ "id": "001"
+ }
+}
+
+native channel SceneUpdateEvent {
+ out scene.time(time: Long, updateEvent(dt: Long)) = time + dt
+}
+
+native channel SceneUpdate {
+ in scene(curSc: Json, update(curSc, nextSc)) = nextSc
+}
+
+native channel CameraPositionUpdate {
+ in scene.camera.transform.position(curPos: Json, updatePosition(nextPos.x, nextPos.y, nextPos.z)) = nextPos
+}
+
+native channel CameraRotationUpdate {
+ in scene.camera.transform.rotation(curRot: Json, updateRotation(nextRot.x, nextRot.y, nextRot.z)) = nextRot
+}
+
+native channel CameraScaleUpdate {
+ in scene.camera.transform.scale(curScale: Json, updateScale(nextScale.x, nextScale.y, nextScale.z)) = nextScale
+}
+
+native channel CameraProjectionUpdate {
+ in scene.camera.projection(curProj: Json, updateProjection(curProj, nextProj)) = nextProj
+}
+
+native channel EntityPositionUpdate(eid: Str) {
+ in scene.entities.{eid}.transform.position(curPos: Json, updatePosition(nextPos.x, nextPos.y, nextPos.z)) = nextPos
+}
+
+native channel EntityRotationUpdate(eid: Str) {
+ in scene.entities.{eid}.transform.rotation(curRot: Json, updateRotation(nextRot.x, nextRot.y, nextRot.z)) = nextRot
+}
+
+native channel EntityScaleUpdate(eid: Str) {
+ in scene.entities.{eid}.transform.scale(curScale: Json, updateScale(nextScale.x, nextScale.y, nextScale.z)) = nextScale
+}
+
+native channel EntitySpriteUpdate(eid: Str) {
+ in scene.entities.{eid}.mesh(curMesh: Json, updateSprite(spritePath: Str)) = {"type": "sprite", "sprite": spritePath}
+}
+
+native channel KeyEvent(kno: Int) {
+ out scene.keys.{kno}.state(curState: Int, keyEvent(nextState)) = nextState
+}
+
+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)
+}
+
+channel AddSprite {
+ out scene.entities(entityDB: Map, addSprite(eid: Str, spritePath: Str)) = insert(entityDB, eid, {
+ "transform": {
+ "position": {"x": 0.0, "y": 0.0, "z": 0.0},
+ "rotation": {"x": 0.0, "y": 0.0, "z": 0.0},
+ "scale": {"x": 1.0, "y": 1.0, "z": 1.0}
+ },
+ "mesh": {"type": "sprite", "sprite": spritePath}
+ })
+}
+
+channel MoveEntity(eid: Str) {
+ out scene.entities.{eid}.transform.position(curPos: Json, move(x: Double, y: Double, z: Double)) = {"x": x, "y": y, "z": z}
+}
+
+channel RotateEntity(eid: Str) {
+ out scene.entities.{eid}.transform.rotation(curRot: Json, rotate(x: Double, y: Double, z: Double)) = {"x": x, "y": y, "z": z}
+}
+
+channel UpdateEnemy(tid: Str) {
+ in timers.{tid}.count(curCount: Long, updateEnemy(nextCount)) = nextCount
+ out enemy.position(curPos: Json, updateEnemy(nextCount)) = {"x": curPos.x, "y": curPos.y + 5, "z": curPos.z}
+ out enemy.rotation(curRot: Json, updateEnemy(nextCount)) = {"x": curRot.x, "y": curRot.y, "z": curRot.z + 5}
+}
+
+channel MoveEnemy {
+ in enemy.position(curPos: Json, moveEnemy(nextPos, nextRot, nextId)) = nextPos
+ in enemy.id(curId: Str, moveEnemy(nextPos, nextRot, nextId)) = nextId
+ out scene.entities.{nextId}.transform.position(curPos: Json, moveEnemy(nextPos, nextRot, nextId)) = nextPos
+}
+
+channel RotateEnemy {
+ in enemy.rotation(curRot: Json, rotateEnemy(nextPos, nextRot, nextId)) = nextRot
+ in enemy.id(curId: Str, rotateEnemy(nextPos, nextRot, nextId)) = nextId
+ out scene.entities.{nextId}.transform.rotation(curRot: Json, rotateEnemy(nextPos, nextRot, nextId)) = nextRot
+}
diff --git a/AlgebraicDataflowArchitectureModel/models/GroupChat.model b/AlgebraicDataflowArchitectureModel/models/GroupChat.model
new file mode 100644
index 0000000..634ddf0
--- /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}}.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/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/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..e003d9a
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/models/SimpleUI.model
@@ -0,0 +1,122 @@
+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 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/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/Test.model b/AlgebraicDataflowArchitectureModel/models/Test.model
deleted file mode 100644
index a8a1348..0000000
--- a/AlgebraicDataflowArchitectureModel/models/Test.model
+++ /dev/null
@@ -1,9 +0,0 @@
-channel CIO {
- out a(x:Int, set(n:Int)) == n
-}
-
-channel C1 {
- in a(x, update(y)) == y
- out b(z, update(y)) == y + 1
- out c(v, update(y)) == v + y
-}
\ No newline at end of file
diff --git a/AlgebraicDataflowArchitectureModel/models/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/WOS.dtram b/AlgebraicDataflowArchitectureModel/models/WOS.dtram
index 45f640c..81b0779 100644
--- a/AlgebraicDataflowArchitectureModel/models/WOS.dtram
+++ b/AlgebraicDataflowArchitectureModel/models/WOS.dtram
@@ -1,17 +1,17 @@
model {
channel CIO2 {
- out highest(h:Double, reset(v)) == v
+ out highest(h:Double, reset(v)) = v
}
channel CIO1 {
- out temp_f(p:Double, observe(x)) == x
+ out temp_f(p:Double, observe(x)) = x
}
channel C1{
- in temp_f(q:Double, conversion(y)) == y
- out temp_c(r:Double, conversion(z)) == (z-32) / 1.8
+ in temp_f(q:Double, conversion(y)) = y
+ out temp_c(r:Double, conversion(z)) = (z-32) / 1.8
}
channel C2{
- in temp_f(q:Double, update(y)) == y
- out highest(h:Double, update(z)) == if(gt(z, h), z, h)
+ in temp_f(q:Double, update(y)) = y
+ out highest(h:Double, update(z)) = if(z >= h, z, h)
}
}
geometry {
diff --git a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model
index 2cd84d7..0096407 100644
--- a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model
+++ b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model
@@ -1,14 +1,14 @@
channel CIO2 {
- out highest(h:Double, reset(v)) == v
+ out highest(h:Double, reset(v)) = v
}
channel CIO1 {
- out temp_f(p:Double, observe(x)) == x
+ out temp_f(p:Double, observe(x)) = x
}
channel C1{
- in temp_f(q:Double, conversion(y)) == y
- out temp_c(r:Double, conversion(z)) == (z-32) / 1.8
+ in temp_f(q:Double, conversion(y)) = y
+ out temp_c(r:Double, conversion(z)) = (z-32) / 1.8
}
channel C2{
- in temp_f(q:Double, update(y)) == y
- out highest(h:Double, update(z)) == if(gt(z, h), z, h)
+ in temp_f(q:Double, update(y)) = y
+ out highest(h:Double, update(z)) = if(z >= h, z, h)
}
diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/DataTransferModelAnalyzer.java b/AlgebraicDataflowArchitectureModel/src/algorithms/DataTransferModelAnalyzer.java
index 836227a..f54aea4 100644
--- a/AlgebraicDataflowArchitectureModel/src/algorithms/DataTransferModelAnalyzer.java
+++ b/AlgebraicDataflowArchitectureModel/src/algorithms/DataTransferModelAnalyzer.java
@@ -24,41 +24,47 @@
*/
static public DataFlowGraph createDataFlowGraphWithStateStoringAttribute(DataTransferModel model) {
DataFlowGraph graph = model.getDataFlowGraph();
- Collection channels = new HashSet<>(model.getIOChannels());
+ Collection channels = new HashSet<>(model.getInputChannels());
channels.addAll(model.getChannels());
for (Channel channel: channels) {
for (ChannelMember member: ((DataTransferChannel) channel).getOutputChannelMembers()) {
- boolean flag = !member.getStateTransition().isRightUnary(); // The state does not need to be stored if the state transition function is right unary.
- for (Node node : graph.getNodes()) {
- if (((ResourceNode) node).getResource().equals(member.getResource())) {
- setStoreAttribute(flag, (ResourceNode) node);
+ boolean toBeStored = !member.getStateTransition().isRightUnary(); // The state does not need to be stored if the state transition function is right unary.
+ for (Node node : graph.getResourceNodes()) {
+ if (((ResourceNode) node).getInSideResources().contains(member.getResource())) {
+ setStoreAttribute((ResourceNode) node, toBeStored);
}
}
}
}
- for (Node node : graph.getNodes()) {
+ for (Node node: graph.getResourceNodes()) {
HashSet inChannels = new HashSet<>();
- for(Edge pre : ((ResourceNode) node).getInEdges()) {
- inChannels.add(((DataFlowEdge) pre).getChannel());
+ for(Edge inEdge: ((ResourceNode) node).getInEdges()) {
+ if (inEdge instanceof DataFlowEdge) {
+ DataFlowEdge dfEdge = (DataFlowEdge) inEdge;
+ if (dfEdge.isChannelToResource()) {
+ inChannels.add(((ChannelNode) dfEdge.getSource()).getChannel());
+ }
+ }
}
if ((inChannels.size() > 1)) {
- setStoreAttribute(true, (ResourceNode) node);
+ // If the resource has multiple input channels, then the state of the resource needs to be stored.
+ setStoreAttribute((ResourceNode) node, true);
} else if (((ResourceNode) node).getAttribute() == null) {
- setStoreAttribute(false, (ResourceNode) node);
+ setStoreAttribute((ResourceNode) node, false);
}
}
return graph;
}
- static private void setStoreAttribute(boolean flag, ResourceNode node) {
+ static private void setStoreAttribute(ResourceNode node, boolean toBeStored) {
NodeAttribute attr = node.getAttribute();
StoreAttribute store;
if (attr != null && attr instanceof NodeAttribute) {
store = (StoreAttribute) attr;
- store.setNeeded(store.isNeeded() || flag);
+ store.setNeeded(store.isNeeded() || toBeStored);
} else {
store = new StoreAttribute();
- store.setNeeded(flag);
+ store.setNeeded(toBeStored);
node.setAttribute(store);
}
}
@@ -69,17 +75,17 @@
* @return annotated data flow graph
*/
static public DataFlowGraph annotateWithSelectableDataTransferAttiribute(DataFlowGraph graph) {
- List nodes = new ArrayList<>(graph.getNodes());
+ List resNodes = new ArrayList<>(graph.getResourceNodes());
// set push only attributes
- for (Node n: graph.getNodes()) {
- if (nodes.contains(n) && ((StoreAttribute) ((ResourceNode) n).getAttribute()).isNeeded()) {
- nodes.remove(n);
- trackEdges(n, nodes);
+ for (Node resNode: graph.getResourceNodes()) {
+ if (resNodes.contains(resNode) && ((StoreAttribute) ((ResourceNode) resNode).getAttribute()).isNeeded()) {
+ resNodes.remove(resNode);
+ trackEdges(resNode, resNodes);
}
}
// set push/pull attributes to the remaining edges
for (Edge e : graph.getEdges()) {
- if (((DataFlowEdge) e).getAttribute() == null) {
+ if (!((DataFlowEdge) e).isChannelToResource() && ((DataFlowEdge) e).getAttribute() == null) {
PushPullAttribute ppat = new PushPullAttribute();
ppat.addOption(PushPullValue.PUSHorPULL);
ppat.addOption(PushPullValue.PUSH);
@@ -90,16 +96,19 @@
return graph;
}
- static private void trackEdges(Node n, List nodes) {
+ static private void trackEdges(Node resNode, List resNodes) {
// recursively set push only attributes to input side edges
- for (Edge e : ((ResourceNode) n).getInEdges()) {
- PushPullAttribute ppat = new PushPullAttribute();
- ppat.addOption(PushPullValue.PUSH);
- ((DataFlowEdge) e).setAttribute(ppat);
- Node n2 = e.getSource();
- if (nodes.contains(n2)) {
- nodes.remove(n2);
- trackEdges(n2, nodes);
+ for (Edge chToRes : ((ResourceNode) resNode).getInEdges()) {
+ Node chNode = chToRes.getSource();
+ for (Edge resToCh : ((ChannelNode) chNode).getInEdges()) {
+ PushPullAttribute ppat = new PushPullAttribute();
+ ppat.addOption(PushPullValue.PUSH);
+ ((DataFlowEdge) resToCh).setAttribute(ppat);
+ Node resNode2 = resToCh.getSource();
+ if (resNodes.contains(resNode2)) {
+ resNodes.remove(resNode2);
+ trackEdges(resNode2, resNodes);
+ }
}
}
}
diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java
index d29070d..ca92529 100644
--- a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java
+++ b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java
@@ -13,6 +13,7 @@
import javax.xml.crypto.Data;
import models.Node;
+import models.algebra.Constant;
import models.algebra.Expression;
import models.algebra.Position;
import models.algebra.Symbol;
@@ -22,7 +23,10 @@
import models.dataConstraintModel.Channel;
import models.dataConstraintModel.ChannelMember;
import models.dataConstraintModel.DataConstraintModel;
+import models.dataConstraintModel.JsonType;
+import models.dataConstraintModel.ResourceHierarchy;
import models.dataConstraintModel.ResourcePath;
+import models.dataConstraintModel.Selector;
import models.dataConstraintModel.StateTransition;
import models.dataFlowModel.DataTransferModel;
import models.dataFlowModel.ResourceNode;
@@ -42,6 +46,8 @@
static private Map pairComponentTypes = new HashMap<>();
static private Map, Type> mapTypes = new HashMap<>();
static private Map> mapComponentTypes = new HashMap<>();
+ static private Map, Type> jsonTypes = new HashMap<>();
+ static private Map> jsonMemberTypes = new HashMap<>();
public static Type getListType(Type compType) {
return listTypes.get(compType);
@@ -83,29 +89,46 @@
return mapComponentTypes.get(mapType);
}
+ public static Type getJsonType(Map memberTypes) {
+ return jsonTypes.get(memberTypes);
+ }
+
+ public static Map getJsonMemberTypes(Type jsonType) {
+ return jsonMemberTypes.get(jsonType);
+ }
+
static public void infer(DataTransferModel model) {
- Map> resources = new HashMap<>();
+ Map> resources = new HashMap<>();
+ Map> resourcePathParams = new HashMap<>();
Map variables = new HashMap<>();
Map, Type>>> messages = new HashMap<>();
Map consOrSet = new HashMap<>();
Map tuple = new HashMap<>();
Map pair = new HashMap<>();
Map map = new HashMap<>();
+ Map json = new HashMap<>();
+
+ // Maps from the objectId of each expression to its belonging group that has the same type as the expression
Map> expToResource = new HashMap<>();
+ Map> expToPathParams = new HashMap<>();
Map> expToVariable = new HashMap<>();
Map> expToMessage = new HashMap<>();
Map>> expToConsOrSet = new HashMap<>();
Map>> expToTuple = new HashMap<>();
Map>> expToPair = new HashMap<>();
Map>> expToMap = new HashMap<>();
+ Map>> expToJson = new HashMap<>();
+ // Maps from the objectId of each group to the set of updated expressions.
Map> updateFromResource = new HashMap<>();
+ Set updateFromResourceOwnership = new HashSet<>();
Map> updateFromVariable = new HashMap<>();
Map> updateFromMessage = new HashMap<>();
Map> updateFromConsOrSet = new HashMap<>();
Map> updateFromTuple = new HashMap<>();
Map> updateFromPair = new HashMap<>();
Map> updateFromMap = new HashMap<>();
+ Map> updateFromJson = new HashMap<>();
listComponentTypes.put(DataConstraintModel.typeList, null);
listComponentTypes.put(DataConstraintModel.typeListInt, DataConstraintModel.typeInt);
@@ -123,813 +146,1121 @@
mapComponentTypes.put(DataConstraintModel.typeMap, Arrays.asList(new Type[] { null, null }));
// 1. Collect type information from the architecture model.
- Collection channels = new HashSet<>(model.getIOChannels());
+ Collection channels = new HashSet<>(model.getInputChannels());
channels.addAll(model.getChannels());
- for (Channel c : channels) {
- for (ChannelMember cm : c.getChannelMembers()) {
- StateTransition st = cm.getStateTransition();
- ResourcePath id = cm.getResource();
-
- // 1.1 Group expressions by resources.
- List sameResource = resources.get(id);
- if (sameResource == null) {
- sameResource = new ArrayList<>();
- resources.put(id, sameResource);
- }
- sameResource.add(st.getCurStateExpression());
- if (st.getNextStateExpression() != null) sameResource.add(st.getNextStateExpression());
- expToResource.put(System.identityHashCode(st.getCurStateExpression()), sameResource);
- if (st.getNextStateExpression() != null) expToResource.put(System.identityHashCode(st.getNextStateExpression()), sameResource);
- Map updatedExps = getUpdateSet(updateFromResource, sameResource);
- Type resType = id.getResourceStateType();
- Expression exp = st.getCurStateExpression();
- Type expType = getExpTypeIfUpdatable(resType, exp);
- if (expType != null) {
- id.setResourceStateType(expType);
- for (Expression resExp : sameResource) {
- if (resExp != exp) {
- if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) {
- ((Variable) resExp).setType(expType);
- updatedExps.put(System.identityHashCode(resExp), resExp);
- } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) {
- ((Term) resExp).setType(expType);
- updatedExps.put(System.identityHashCode(resExp), resExp);
- }
+ for (Channel ch : channels) {
+ // 1.1 Group expressions by resources.
+ IGroupExpressionsByResource groupExpressionsByResource = new IGroupExpressionsByResource() {
+ public void groupForChannel(Channel ch) {
+ for (ChannelMember cm : ch.getChannelMembers()) {
+ StateTransition st = cm.getStateTransition();
+ ResourceHierarchy res = cm.getResource().getResourceHierarchy();
+ List identicalResources = resources.get(res);
+ if (identicalResources == null) {
+ identicalResources = new ArrayList<>();
+ resources.put(res, identicalResources);
}
- }
- } else if (exp instanceof Variable) {
- if (compareTypes(((Variable) exp).getType(), resType)) {
- ((Variable) exp).setType(resType);
- updatedExps.put(System.identityHashCode(exp), exp);
- }
- } else if (exp instanceof Term) {
- if (compareTypes(((Term) exp).getType(), resType)) {
- ((Term) exp).setType(resType);
- updatedExps.put(System.identityHashCode(exp), exp);
- }
- }
- resType = id.getResourceStateType();
- exp = st.getNextStateExpression();
- if (exp != null) {
- expType = getExpTypeIfUpdatable(resType, exp);
- if (expType != null) {
- id.setResourceStateType(expType);
- for (Expression resExp : sameResource) {
- if (resExp != exp) {
- if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) {
- ((Variable) resExp).setType(expType);
- updatedExps.put(System.identityHashCode(resExp), resExp);
- } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) {
- ((Term) resExp).setType(expType);
- updatedExps.put(System.identityHashCode(resExp), resExp);
- }
- }
+ identicalResources.add(st.getCurStateExpression());
+ expToResource.put(System.identityHashCode(st.getCurStateExpression()), identicalResources);
+ if (st.getNextStateExpression() != null) {
+ identicalResources.add(st.getNextStateExpression());
+ expToResource.put(System.identityHashCode(st.getNextStateExpression()), identicalResources);
}
- } else if (exp instanceof Variable) {
- if (compareTypes(((Variable) exp).getType(), resType)) {
- ((Variable) exp).setType(resType);
- updatedExps.put(System.identityHashCode(exp), exp);
- }
- } else if (exp instanceof Term) {
- if (compareTypes(((Term) exp).getType(), resType)) {
- ((Term) exp).setType(resType);
- updatedExps.put(System.identityHashCode(exp), exp);
- }
- }
- }
-
- // 1.2 Group expressions by variable.
- Map> locals = new HashMap<>();
- Map localTypes = new HashMap<>();
- List allVariables = new ArrayList<>();
- allVariables.addAll(st.getCurStateExpression().getVariables().values());
- allVariables.addAll(st.getMessageExpression().getVariables().values());
- if (st.getNextStateExpression() != null)
- allVariables.addAll(st.getNextStateExpression().getVariables().values());
- for (Variable var : allVariables) {
- List sameVariable = locals.get(var.getName());
- if (sameVariable == null) {
- sameVariable = new ArrayList<>();
- sameVariable.add(var);
- expToVariable.put(System.identityHashCode(var), sameVariable);
- locals.put(var.getName(), sameVariable);
- localTypes.put(var.getName(), var.getType());
- } else {
- sameVariable.add(var);
- expToVariable.put(System.identityHashCode(var), sameVariable);
- Type varType = localTypes.get(var.getName());
- Map updatedVars = getUpdateSet(updateFromVariable, sameVariable);
- if (compareTypes(varType, var.getType())) {
- localTypes.put(var.getName(), var.getType());
- for (Expression v : sameVariable) {
- if (v != var) {
- if (compareTypes(((Variable) v).getType(), var.getType())) {
- ((Variable) v).setType(var.getType());
- updatedVars.put(System.identityHashCode(v), v);
+ Map updatedExps = getUpdateSet(updateFromResource, identicalResources);
+ Type resType = res.getResourceStateType();
+ Expression exp = st.getCurStateExpression();
+ Type expType = getExpTypeIfUpdatable(resType, exp);
+ if (expType != null) {
+ res.setResourceStateType(expType);
+ for (Expression resExp : identicalResources) {
+ if (resExp != exp) {
+ if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) {
+ ((Variable) resExp).setType(expType);
+ updatedExps.put(System.identityHashCode(resExp), resExp);
+ } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) {
+ ((Term) resExp).setType(expType);
+ updatedExps.put(System.identityHashCode(resExp), resExp);
}
}
}
- } else if (compareTypes(var.getType(), varType)) {
- var.setType(varType);
- updatedVars.put(System.identityHashCode(var), var);
- }
- }
- }
- for (String varName : locals.keySet()) {
- variables.put(System.identityHashCode(locals.get(varName)), localTypes.get(varName));
- }
-
- // 1.3 Group expressions by message.
- Expression message = st.getMessageExpression();
- if (message instanceof Variable) {
- Type msgType = ((Variable) message).getType();
- Map, Type>> msgTypeMap = messages.get(c);
- if (msgTypeMap == null) {
- msgTypeMap = new HashMap<>();
- messages.put(c, msgTypeMap);
- }
- Map.Entry, Type> typeAndExps = msgTypeMap.get(0);
- if (typeAndExps == null) {
- List exps = new ArrayList<>();
- exps.add(message);
- typeAndExps = new AbstractMap.SimpleEntry<>(exps, msgType);
- msgTypeMap.put(0, typeAndExps);
- expToMessage.put(System.identityHashCode(message), exps);
- } else {
- typeAndExps.getKey().add(message);
- expToMessage.put(System.identityHashCode(message), typeAndExps.getKey());
- Map updateExps = getUpdateSet(updateFromMessage, typeAndExps.getKey());
- if (compareTypes(typeAndExps.getValue(), msgType)) {
- typeAndExps.setValue(msgType);
- for (Expression e : typeAndExps.getKey()) {
- if (e != message) {
- if (e instanceof Variable) {
- ((Variable) e).setType(msgType);
- updateExps.put(System.identityHashCode(e), e);
- }
- }
+ } else if (exp instanceof Variable) {
+ if (compareTypes(((Variable) exp).getType(), resType)) {
+ ((Variable) exp).setType(resType);
+ updatedExps.put(System.identityHashCode(exp), exp);
}
- } else if (compareTypes(msgType, typeAndExps.getValue())) {
- ((Variable) message).setType(typeAndExps.getValue());
- updateExps.put(System.identityHashCode(message), message);
+ } else if (exp instanceof Term) {
+ if (compareTypes(((Term) exp).getType(), resType)) {
+ ((Term) exp).setType(resType);
+ updatedExps.put(System.identityHashCode(exp), exp);
+ }
}
- }
- } else if (message instanceof Term) {
- Map, Type>> msgTypeMap = messages.get(c);
- if (msgTypeMap == null) {
- msgTypeMap = new HashMap<>();
- messages.put(c, msgTypeMap);
- }
- for (int i = 0; i < ((Term) message).getArity(); i++) {
- Expression arg = ((Term) message).getChild(i);
- Type argType = null;
- if (arg instanceof Variable) {
- argType = ((Variable) arg).getType();
- } else if (arg instanceof Term) {
- argType = ((Term) arg).getType();
- } else {
- continue;
- }
- Map.Entry, Type> typeAndExps = msgTypeMap.get(i);
- if (typeAndExps == null) {
- List exps = new ArrayList<>();
- exps.add(arg);
- typeAndExps = new AbstractMap.SimpleEntry<>(exps, argType);
- msgTypeMap.put(i, typeAndExps);
- expToMessage.put(System.identityHashCode(arg), exps);
- } else {
- typeAndExps.getKey().add(arg);
- expToMessage.put(System.identityHashCode(arg), typeAndExps.getKey());
- Map updateExps = getUpdateSet(updateFromMessage, typeAndExps.getKey());
- if (compareTypes(typeAndExps.getValue(), argType)) {
- typeAndExps.setValue(argType);
- for (Expression e : typeAndExps.getKey()) {
- if (e != arg) {
- if (e instanceof Variable) {
- ((Variable) e).setType(argType);
- updateExps.put(System.identityHashCode(e), e);
+ resType = res.getResourceStateType();
+ exp = st.getNextStateExpression();
+ if (exp != null) {
+ expType = getExpTypeIfUpdatable(resType, exp);
+ if (expType != null) {
+ res.setResourceStateType(expType);
+ for (Expression resExp : identicalResources) {
+ if (resExp != exp) {
+ if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) {
+ ((Variable) resExp).setType(expType);
+ updatedExps.put(System.identityHashCode(resExp), resExp);
+ } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) {
+ ((Term) resExp).setType(expType);
+ updatedExps.put(System.identityHashCode(resExp), resExp);
}
}
}
- } else if (compareTypes(argType, typeAndExps.getValue())) {
- if (arg instanceof Variable) {
- ((Variable) arg).setType(typeAndExps.getValue());
- updateExps.put(System.identityHashCode(arg), arg);
- } else if (arg instanceof Term) {
- ((Term) arg).setType(typeAndExps.getValue());
- updateExps.put(System.identityHashCode(arg), arg);
+ } else if (exp instanceof Variable) {
+ if (compareTypes(((Variable) exp).getType(), resType)) {
+ ((Variable) exp).setType(resType);
+ updatedExps.put(System.identityHashCode(exp), exp);
+ }
+ } else if (exp instanceof Term) {
+ if (compareTypes(((Term) exp).getType(), resType)) {
+ ((Term) exp).setType(resType);
+ updatedExps.put(System.identityHashCode(exp), exp);
}
}
}
+ }
+ for (Channel childCh: ch.getChildren()) {
+ groupForChannel(childCh);
}
}
+ };
+ groupExpressionsByResource.groupForChannel(ch);
- // 1.4 Extract constraints on expressions in each term.
- List terms = new ArrayList<>();
- if (st.getCurStateExpression() instanceof Term) {
- Map subTerms = ((Term) st.getCurStateExpression()).getSubTerms(Term.class);
- terms.addAll(subTerms.values());
- }
- if (st.getMessageExpression() instanceof Term) {
- Map subTerms = ((Term) st.getMessageExpression()).getSubTerms(Term.class);
- terms.addAll(subTerms.values());
- }
- if (st.getNextStateExpression() != null && st.getNextStateExpression() instanceof Term) {
- Map subTerms = ((Term) st.getNextStateExpression()).getSubTerms(Term.class);
- terms.addAll(subTerms.values());
- }
- for (Term t : terms) {
- Symbol symbol = t.getSymbol();
- if (symbol.equals(DataConstraintModel.cons) || symbol.equals(DataConstraintModel.set)) {
- // If the root symbol of the term is cons or set.
- List consExps = new ArrayList<>();
- consExps.add(t);
- updateExpressionBelonging(expToConsOrSet, t, consExps);
- if (symbol.equals(DataConstraintModel.cons)) {
- // If the root symbol of the term is cons.
- for (Expression e : t.getChildren()) {
- consExps.add(e);
- updateExpressionBelonging(expToConsOrSet, e, consExps);
- }
- } else {
- // If the root symbol of the term is set.
- Expression e = t.getChildren().get(2);
- consExps.add(e);
- updateExpressionBelonging(expToConsOrSet, e, consExps);
- e = t.getChildren().get(0);
- consExps.add(e);
- updateExpressionBelonging(expToConsOrSet, e, consExps);
+ // 1.2 Group expressions by variable.
+ IGroupExpressionsByVariable groupExpressionsByVariable = new IGroupExpressionsByVariable() {
+ public void groupForChannel(Channel ch) {
+ for (ChannelMember cm : ch.getChannelMembers()) {
+ StateTransition st = cm.getStateTransition();
+ Map> locals = new HashMap<>();
+ Map localTypes = new HashMap<>();
+ List allVariables = new ArrayList<>();
+ allVariables.addAll(st.getCurStateExpression().getVariables().values());
+ allVariables.addAll(st.getMessageExpression().getVariables().values());
+ if (st.getNextStateExpression() != null) {
+ allVariables.addAll(st.getNextStateExpression().getVariables().values());
}
- Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2));
- if (newType != null) {
- // If the type of the 2nd argument of cons (1st argument of set) is more concrete than the type of the term.
- t.setType(newType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(t), t);
- } else {
- Type arg2Type = null;
- if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
- arg2Type = ((Variable) consExps.get(2)).getType();
- if (compareTypes(arg2Type, t.getType())) {
- // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set).
- ((Variable) consExps.get(2)).setType(t.getType());
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
- }
- } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
- arg2Type = ((Term) consExps.get(2)).getType();
- if (compareTypes(arg2Type, t.getType())) {
- // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set).
- ((Term) consExps.get(2)).setType(t.getType());
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
- }
+ for (Selector s: ch.getAllSelectors()) { // add channel selectors
+ if (s.getExpression() instanceof Variable) {
+ allVariables.add((Variable) s.getExpression());
}
}
- Type newCompType = getExpTypeIfUpdatable(listComponentTypes.get(t.getType()), consExps.get(1));
- if (newCompType != null) {
- // If the type of the 1st argument of cons (3rd argument of set) is more concrete than the type of list component.
- Type newListType = listTypes.get(newCompType);
- if (newListType == null) {
- // Create new list type.
- newListType = createNewListType(newCompType, DataConstraintModel.typeList);
- }
- t.setType(newListType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(t), t);
- if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
- ((Variable) consExps.get(2)).setType(newListType);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
- } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
- ((Term) consExps.get(2)).setType(newListType);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ ResourcePath resPath = cm.getResource();
+ for (Expression param: resPath.getPathParams()) { // add path parameters
+ if (param instanceof Variable) {
+ allVariables.add((Variable) param);
+ } else if (param instanceof Term) {
+ allVariables.addAll(((Term) param).getVariables().values());
}
}
- consOrSet.put(System.identityHashCode(consExps), t.getType());
- } else if (symbol.equals(DataConstraintModel.head) || symbol.equals(DataConstraintModel.get)) {
- // If the root symbol of the term is head or get.
- List consExps = new ArrayList<>();
- Expression e = t.getChildren().get(0);
- consExps.add(e);
- updateExpressionBelonging(expToConsOrSet, e, consExps);
- consExps.add(t);
- updateExpressionBelonging(expToConsOrSet, t, consExps);
- consExps.add(null);
- Type listType = listTypes.get(t.getType());
- if (listType == null && t.getType() != null) {
- // Create a new list type.
- listType = createNewListType(t.getType(), DataConstraintModel.typeList);
- }
- Type newListType = getExpTypeIfUpdatable(listType, consExps.get(0));
- if (newListType != null) {
- // If the type of the component of the 1st argument is more concrete than the type of the term.
- Type newCompType = listComponentTypes.get(newListType);
- if (newCompType != null) {
- t.setType(newCompType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(t), t);
- }
- consOrSet.put(System.identityHashCode(consExps), newListType);
- } else {
- // If the type of the term is more concrete than the type of the component of the 1st argument.
- if (consExps.get(0) != null && consExps.get(0) instanceof Variable) {
- ((Variable) consExps.get(0)).setType(listType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0));
- } else if (consExps.get(0) != null && consExps.get(0) instanceof Term) {
- ((Term) consExps.get(0)).setType(listType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0));
- }
- consOrSet.put(System.identityHashCode(consExps), listType);
- }
- } else if (symbol.equals(DataConstraintModel.tail)) {
- // If the root symbol of the term is tail.
- List consExps = new ArrayList<>();
- consExps.add(t);
- updateExpressionBelonging(expToConsOrSet, t, consExps);
- consExps.add(null);
- Expression e = t.getChildren().get(0);
- consExps.add(e);
- updateExpressionBelonging(expToConsOrSet, e, consExps);
- Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2));
- if (newType != null) {
- // If the type of the argument is more concrete than the type of the term.
- t.setType(newType);
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(t), t);
- } else {
- Type argType = null;
- if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
- argType = ((Variable) consExps.get(2)).getType();
- if (compareTypes(argType, t.getType())) {
- // If the type of the term is more concrete than the type of the argument.
- ((Variable) consExps.get(2)).setType(t.getType());
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
- }
- } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
- argType = ((Term) consExps.get(2)).getType();
- if (compareTypes(argType, t.getType())) {
- // If the type of the term is more concrete than the type of the argument.
- ((Term) consExps.get(2)).setType(t.getType());
- Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
- updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
- }
- }
- }
- consOrSet.put(System.identityHashCode(consExps), t.getType());
- } else if (symbol.equals(DataConstraintModel.tuple)) {
- // If the root symbol of the term is tuple.
- List tupleExps = new ArrayList<>();
- List argsTypeList = new ArrayList<>();
- tupleExps.add(t);
- updateExpressionBelonging(expToTuple, t, tupleExps);
- for (Expression e : t.getChildren()) {
- tupleExps.add(e);
- updateExpressionBelonging(expToTuple, e, tupleExps);
- if (e instanceof Variable) {
- argsTypeList.add(((Variable) e).getType());
- } else if (e instanceof Term) {
- argsTypeList.add(((Term) e).getType());
+ for (Variable var : allVariables) {
+ List sameVariable = locals.get(var.getName());
+ if (sameVariable == null) {
+ sameVariable = new ArrayList<>();
+ sameVariable.add(var);
+ expToVariable.put(System.identityHashCode(var), sameVariable);
+ locals.put(var.getName(), sameVariable);
+ localTypes.put(var.getName(), var.getType());
} else {
- argsTypeList.add(null);
+ sameVariable.add(var);
+ expToVariable.put(System.identityHashCode(var), sameVariable);
+ Type varType = localTypes.get(var.getName());
+ Map updatedVars = getUpdateSet(updateFromVariable, sameVariable);
+ if (compareTypes(varType, var.getType())) {
+ localTypes.put(var.getName(), var.getType());
+ for (Expression v : sameVariable) {
+ if (v != var) {
+ if (compareTypes(((Variable) v).getType(), var.getType())) {
+ ((Variable) v).setType(var.getType());
+ updatedVars.put(System.identityHashCode(v), v);
+ }
+ }
+ }
+ } else if (compareTypes(var.getType(), varType)) {
+ var.setType(varType);
+ updatedVars.put(System.identityHashCode(var), var);
+ }
}
}
- if (t.getType() == DataConstraintModel.typeTuple) {
- Type newTupleType = tupleTypes.get(argsTypeList);
- if (newTupleType == null) {
- // Create new tuple type;
- newTupleType = createNewTupleType(argsTypeList, DataConstraintModel.typeTuple);
- }
- t.setType(newTupleType);
- Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
- updateExps.put(System.identityHashCode(t), t);
+ for (String varName : locals.keySet()) {
+ variables.put(System.identityHashCode(locals.get(varName)), localTypes.get(varName));
}
- tuple.put(System.identityHashCode(tupleExps), t.getType());
- } else if (symbol.equals(DataConstraintModel.pair)) {
- // If the root symbol of the term is pair.
- List pairExps = new ArrayList<>();
- pairExps.add(t);
- updateExpressionBelonging(expToPair, t, pairExps);
- if (t.getType() == DataConstraintModel.typePair) {
- for (Expression e : t.getChildren()) {
- pairExps.add(e);
- updateExpressionBelonging(expToPair, e, pairExps);
+ }
+ for (Channel childCh: ch.getChildren()) {
+ groupForChannel(childCh);
+ }
+ }
+ };
+ groupExpressionsByVariable.groupForChannel(ch);
+
+ // 1.3 Group expressions by message.
+ IGroupExpressionsByMessage groupExpressionsByMessage = new IGroupExpressionsByMessage() {
+ public void groupForChannel(Channel rootCh, Channel ch) {
+ for (ChannelMember cm : ch.getChannelMembers()) {
+ Expression message = cm.getStateTransition().getMessageExpression();
+ if (message instanceof Variable) {
+ Type msgType = ((Variable) message).getType();
+ Map, Type>> msgTypeMap = messages.get(rootCh);
+ if (msgTypeMap == null) {
+ msgTypeMap = new HashMap<>();
+ messages.put(rootCh, msgTypeMap);
+ }
+ Map.Entry, Type> typeAndExps = msgTypeMap.get(0);
+ if (typeAndExps == null) {
+ List exps = new ArrayList<>();
+ exps.add(message);
+ typeAndExps = new AbstractMap.SimpleEntry<>(exps, msgType);
+ msgTypeMap.put(0, typeAndExps);
+ expToMessage.put(System.identityHashCode(message), exps);
+ } else {
+ typeAndExps.getKey().add(message);
+ expToMessage.put(System.identityHashCode(message), typeAndExps.getKey());
+ Map updateExps = getUpdateSet(updateFromMessage, typeAndExps.getKey());
+ if (compareTypes(typeAndExps.getValue(), msgType)) {
+ typeAndExps.setValue(msgType);
+ for (Expression e : typeAndExps.getKey()) {
+ if (e != message) {
+ if (e instanceof Variable) {
+ ((Variable) e).setType(msgType);
+ updateExps.put(System.identityHashCode(e), e);
+ }
+ }
+ }
+ } else if (compareTypes(msgType, typeAndExps.getValue())) {
+ ((Variable) message).setType(typeAndExps.getValue());
+ updateExps.put(System.identityHashCode(message), message);
+ }
+ }
+ } else if (message instanceof Term) {
+ Map, Type>> msgTypeMap = messages.get(rootCh);
+ if (msgTypeMap == null) {
+ msgTypeMap = new HashMap<>();
+ messages.put(rootCh, msgTypeMap);
+ }
+ for (int i = 0; i < ((Term) message).getArity(); i++) {
+ Expression arg = ((Term) message).getChild(i);
Type argType = null;
- if (e instanceof Variable) {
- argType = (((Variable) e).getType());
-
- } else if (e instanceof Term) {
- argType = (((Term) e).getType());
- }
-
- if (argType != null) {
- Type newPairType = pairTypes.get(argType);
- if (newPairType != null) {
- t.setType(newPairType);
- Map updateExps = getUpdateSet(updateFromPair, pairExps);
- updateExps.put(System.identityHashCode(t), t);
- }
- }
- }
- pair.put(System.identityHashCode(pairExps), t.getType());
-
- }
- } else if (symbol.equals(DataConstraintModel.fst)) {
- // If the root symbol of the term is fst.
- List tupleExps = new ArrayList<>();
- Expression arg = t.getChildren().get(0);
- tupleExps.add(arg);
- updateExpressionBelonging(expToTuple, arg, tupleExps);
- tupleExps.add(t);
- updateExpressionBelonging(expToTuple, t, tupleExps);
- tupleExps.add(null);
- Type argType = null;
- if (arg instanceof Variable) {
- argType = ((Variable) arg).getType();
- } else if (arg instanceof Term) {
- argType = ((Term) arg).getType();
- }
- Type newTupleType = DataConstraintModel.typeTuple;
- if (argType == DataConstraintModel.typeTuple && t.getType() != null) {
- List compTypeList = new ArrayList<>();
- compTypeList.add(t.getType());
- compTypeList.add(null);
- newTupleType = tupleTypes.get(compTypeList);
- if (newTupleType == null) {
- // Create new tuple type;
- newTupleType = createNewTupleType(compTypeList, DataConstraintModel.typeTuple);
- }
- }
- if (argType != newTupleType && newTupleType != null) {
- if (arg instanceof Variable) {
- ((Variable) arg).setType(newTupleType);
- argType = newTupleType;
- } else if (arg instanceof Term) {
- ((Term) arg).setType(newTupleType);
- argType = newTupleType;
- }
- Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
- updateExps.put(System.identityHashCode(arg), arg);
- }
- tuple.put(System.identityHashCode(tupleExps), argType);
- } else if (symbol.equals(DataConstraintModel.snd)) {
- // If the root symbol of the term is snd.
- List tupleExps = new ArrayList<>();
- Expression arg = t.getChildren().get(0);
- tupleExps.add(arg);
- updateExpressionBelonging(expToTuple, arg, tupleExps);
- tupleExps.add(null);
- tupleExps.add(t);
- updateExpressionBelonging(expToTuple, t, tupleExps);
- Type argType = null;
- if (arg instanceof Variable) {
- argType = ((Variable) arg).getType();
- } else if (arg instanceof Term) {
- argType = ((Term) arg).getType();
- }
- Type newTupleType = DataConstraintModel.typeTuple;
- if (argType == DataConstraintModel.typeTuple && t.getType() != null) {
- List compTypeList = new ArrayList<>();
- compTypeList.add(null);
- if (DataConstraintModel.typeTuple.isAncestorOf(t.getType())) {
- List sndTypes = tupleComponentTypes.get(t.getType());
- if (sndTypes != null) {
- for (Type t2: sndTypes) {
- compTypeList.add(t2);
- }
+ if (arg instanceof Variable) {
+ argType = ((Variable) arg).getType();
+ } else if (arg instanceof Term) {
+ argType = ((Term) arg).getType();
} else {
- compTypeList.add(t.getType());
+ continue;
}
- } else {
- compTypeList.add(t.getType());
- }
- newTupleType = tupleTypes.get(compTypeList);
- if (newTupleType == null) {
- // Create new tuple type;
- newTupleType = createNewTupleType(compTypeList, DataConstraintModel.typeTuple);
- }
- }
- if (argType != newTupleType && newTupleType != null) {
- if (arg instanceof Variable) {
- ((Variable) arg).setType(newTupleType);
- argType = newTupleType;
- } else if (arg instanceof Term) {
- ((Term) arg).setType(newTupleType);
- argType = newTupleType;
- }
- Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
- updateExps.put(System.identityHashCode(arg), arg);
- }
- tuple.put(System.identityHashCode(tupleExps), argType);
- } else if (symbol.equals(DataConstraintModel.left)) {
- // If the root symbol of the term is left.
- List pairExps = new ArrayList<>();
- Expression arg = t.getChildren().get(0);
- pairExps.add(arg);
- updateExpressionBelonging(expToPair, arg, pairExps);
- pairExps.add(t);
- updateExpressionBelonging(expToPair, t, pairExps);
- pairExps.add(null);
- Type argType = null;
- if (arg instanceof Variable) {
- argType = ((Variable) arg).getType();
- } else if (arg instanceof Term) {
- argType = ((Term) arg).getType();
- }
- Type newPairType = DataConstraintModel.typePair;
- if (argType == DataConstraintModel.typePair && t.getType() != null) {
- List compTypeList = new ArrayList<>();
- compTypeList.add(t.getType());
- compTypeList.add(null);
- newPairType = pairTypes.get(compTypeList);
- if (newPairType == null) {
- // Create new tuple type;
- newPairType = createNewTupleType(compTypeList, DataConstraintModel.typePair);
- }
- }
- if (argType != newPairType && newPairType != null) {
- if (arg instanceof Variable) {
- ((Variable) arg).setType(newPairType);
- argType = newPairType;
- } else if (arg instanceof Term) {
- ((Term) arg).setType(newPairType);
- argType = newPairType;
- }
- Map updateExps = getUpdateSet(updateFromPair, pairExps);
- updateExps.put(System.identityHashCode(arg), arg);
- }
- pair.put(System.identityHashCode(pairExps), argType);
- } else if (symbol.equals(DataConstraintModel.right)) {
- // If the root symbol of the term is right.
- List pairExps = new ArrayList<>();
- Expression arg = t.getChildren().get(0);
- pairExps.add(arg);
- updateExpressionBelonging(expToPair, arg, pairExps);
- pairExps.add(null);
- pairExps.add(t);
- updateExpressionBelonging(expToPair, t, pairExps);
- Type argType = null;
- if (arg instanceof Variable) {
- argType = ((Variable) arg).getType();
- } else if (arg instanceof Term) {
- argType = ((Term) arg).getType();
- }
- Type newPairType = DataConstraintModel.typePair;
- if (argType == DataConstraintModel.typePair && t.getType() != null) {
- List compTypeList = new ArrayList<>();
- compTypeList.add(null);
- compTypeList.add(t.getType());
- newPairType = pairTypes.get(compTypeList);
- if (newPairType == null) {
- // Create new tuple type;
- newPairType = createNewTupleType(compTypeList, DataConstraintModel.typePair);
- }
- }
- if (argType != newPairType && newPairType != null) {
- if (arg instanceof Variable) {
- ((Variable) arg).setType(newPairType);
- argType = newPairType;
- } else if (arg instanceof Term) {
- ((Term) arg).setType(newPairType);
- argType = newPairType;
- }
- Map updateExps = getUpdateSet(updateFromPair, pairExps);
- updateExps.put(System.identityHashCode(arg), arg);
- }
- pair.put(System.identityHashCode(pairExps), argType);
- } else if (symbol.equals(DataConstraintModel.lookup)) {
- // If the root symbol of the term is lookup.
- List mapExps = new ArrayList<>();
- Expression arg1 = t.getChildren().get(0); // map
- mapExps.add(arg1);
- updateExpressionBelonging(expToMap, arg1, mapExps);
- Expression arg2 = t.getChildren().get(1); // key
- mapExps.add(arg2);
- updateExpressionBelonging(expToMap, arg2, mapExps);
- mapExps.add(t); // value
- updateExpressionBelonging(expToMap, t, mapExps);
- Type arg1Type = null;
- if (arg1 instanceof Variable) {
- arg1Type = ((Variable) arg1).getType();
- } else if (arg1 instanceof Term) {
- arg1Type = ((Term) arg1).getType();
- }
- List compTypeList = new ArrayList<>();
- if (arg2 instanceof Variable) {
- compTypeList.add(((Variable) arg2).getType());
- } else if (arg2 instanceof Term) {
- compTypeList.add(((Term) arg2).getType());
- } else {
- compTypeList.add(null);
- }
- compTypeList.add(t.getType());
- if (arg1Type == DataConstraintModel.typeMap || arg1Type == null) {
- Type newMapType = mapTypes.get(compTypeList);
- if (newMapType == null) {
- // Create new tuple type;
- newMapType = createNewMapType(compTypeList, DataConstraintModel.typeMap);
- }
- if (arg1 instanceof Variable) {
- ((Variable) arg1).setType(newMapType);
- arg1Type = newMapType;
- } else if (arg1 instanceof Term) {
- ((Term) arg1).setType(newMapType);
- arg1Type = newMapType;
- }
- Map updateExps = getUpdateSet(updateFromMap, mapExps);
- updateExps.put(System.identityHashCode(arg1), arg1);
- }
- map.put(System.identityHashCode(mapExps), arg1Type);
- } else if (symbol.equals(DataConstraintModel.insert)) {
- // If the root symbol of the term is insert.
- List mapExps = new ArrayList<>();
- mapExps.add(t); // map
- updateExpressionBelonging(expToMap, t, mapExps);
- Expression arg1 = t.getChildren().get(1); // key
- mapExps.add(arg1);
- updateExpressionBelonging(expToMap, arg1, mapExps);
- Expression arg2 = t.getChildren().get(2); // value
- mapExps.add(arg2);
- updateExpressionBelonging(expToMap, arg2, mapExps);
- Expression arg0 = t.getChildren().get(0); // map
- mapExps.add(arg0);
- updateExpressionBelonging(expToMap, arg0, mapExps);
- Type termType = t.getType();
- List compTypeList = new ArrayList<>();
- if (arg1 instanceof Variable) {
- compTypeList.add(((Variable) arg1).getType());
- } else if (arg1 instanceof Term) {
- compTypeList.add(((Term) arg1).getType());
- } else {
- compTypeList.add(null);
- }
- if (arg2 instanceof Variable) {
- compTypeList.add(((Variable) arg2).getType());
- } else if (arg2 instanceof Term) {
- compTypeList.add(((Term) arg2).getType());
- } else {
- compTypeList.add(null);
- }
- if (termType == DataConstraintModel.typeMap || termType == null) {
- Type newMapType = mapTypes.get(compTypeList);
- if (newMapType == null) {
- // Create new tuple type;
- newMapType = createNewMapType(compTypeList, DataConstraintModel.typeMap);
- }
- t.setType(newMapType);
- termType = newMapType;
- Map updateExps = getUpdateSet(updateFromMap, mapExps);
- updateExps.put(System.identityHashCode(t), t);
- }
- map.put(System.identityHashCode(mapExps), termType);
- } else if (symbol.equals(DataConstraintModel.cond)) {
- // If the root symbol of the term is if function.
- Expression c1 = t.getChild(1);
- Expression c2 = t.getChild(2);
- List condTerms = new ArrayList<>();
- condTerms.add(t);
- condTerms.add(c1);
- condTerms.add(c2);
- expToVariable.put(System.identityHashCode(t), condTerms);
- expToVariable.put(System.identityHashCode(c1), condTerms);
- expToVariable.put(System.identityHashCode(c2), condTerms);
- Type condType = t.getType();
- Map updatedVars = getUpdateSet(updateFromVariable, condTerms);
- Type child1Type = getExpTypeIfUpdatable(condType, c1);
- if (child1Type != null) {
- condType = child1Type;
- t.setType(child1Type);
- updatedVars.put(System.identityHashCode(t), t);
- } else {
- if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), condType)) {
- ((Variable) c1).setType(condType);
- updatedVars.put(System.identityHashCode(c1), c1);
- } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), condType)) {
- ((Term) c1).setType(condType);
- updatedVars.put(System.identityHashCode(c1), c1);
- }
- }
- Type child2Type = getExpTypeIfUpdatable(condType, c2);
- if (child2Type != null) {
- condType = child2Type;
- t.setType(child2Type);
- updatedVars.put(System.identityHashCode(t), t);
- if (c1 instanceof Variable) {
- ((Variable) c1).setType(child2Type);
- updatedVars.put(System.identityHashCode(c1), c1);
- } else if (c1 instanceof Term) {
- ((Term) c1).setType(child2Type);
- updatedVars.put(System.identityHashCode(c1), c1);
- }
- } else {
- if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), condType)) {
- ((Variable) c2).setType(condType);
- updatedVars.put(System.identityHashCode(c2), c2);
- } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), condType)) {
- ((Term) c2).setType(condType);
- updatedVars.put(System.identityHashCode(c2), c2);
- }
- }
- variables.put(System.identityHashCode(condTerms), condType);
- } else if (symbol.equals(DataConstraintModel.add) || symbol.equals(DataConstraintModel.sub)
- || symbol.equals(DataConstraintModel.mul) || symbol.equals(DataConstraintModel.div)) {
- // If the root symbol of the term is arithmetic operators.
- Expression c1 = t.getChild(0);
- Expression c2 = t.getChild(1);
- List operands = new ArrayList<>();
- operands.add(t);
- operands.add(c1);
- operands.add(c2);
- expToVariable.put(System.identityHashCode(t), operands);
- expToVariable.put(System.identityHashCode(c1), operands);
- expToVariable.put(System.identityHashCode(c2), operands);
- Type opType = t.getType();
- Map updatedVars = getUpdateSet(updateFromVariable, operands);
- Type child1Type = getExpTypeIfUpdatable(opType, c1);
- if (child1Type != null) {
- opType = child1Type;
- t.setType(child1Type);
- updatedVars.put(System.identityHashCode(t), t);
- } else {
- if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), opType)) {
- ((Variable) c1).setType(opType);
- updatedVars.put(System.identityHashCode(c1), c1);
- } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), opType)) {
- ((Term) c1).setType(opType);
- updatedVars.put(System.identityHashCode(c1), c1);
- }
- }
- Type child2Type = getExpTypeIfUpdatable(opType, c2);
- if (child2Type != null) {
- opType = child2Type;
- t.setType(child2Type);
- updatedVars.put(System.identityHashCode(t), t);
- if (c1 instanceof Variable) {
- ((Variable) c1).setType(child2Type);
- updatedVars.put(System.identityHashCode(c1), c1);
- } else if (c1 instanceof Term) {
- ((Term) c1).setType(child2Type);
- updatedVars.put(System.identityHashCode(c1), c1);
- }
- } else {
- if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), opType)) {
- ((Variable) c2).setType(opType);
- updatedVars.put(System.identityHashCode(c2), c2);
- } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), opType)) {
- ((Term) c2).setType(opType);
- updatedVars.put(System.identityHashCode(c2), c2);
- }
- }
- variables.put(System.identityHashCode(operands), opType);
- } else if (symbol.getSignature() != null
- && symbol.getSignature()[0] == DataConstraintModel.typeList) {
- // If the root symbol of the term is the list type (except for the cons
- // function).
- List consExps = new ArrayList<>();
- consExps.add(t);
- expToVariable.put(System.identityHashCode(t), consExps);
- Type condType = t.getType();
- Map updatedVars = getUpdateSet(updateFromVariable, consExps);
- for (int i = 1; i < symbol.getSignature().length; i++) {
- Type tc = symbol.getSignature()[i];
- if (tc == DataConstraintModel.typeList) {
- Expression e = t.getChildren().get(i - 1);
- Type newType = getExpTypeIfUpdatable(condType, e);
- if (newType != null) {
- condType = newType;
- for (Expression e2 : consExps) {
- if (e2 instanceof Variable) {
- ((Variable) e2).setType(newType);
- updatedVars.put(System.identityHashCode(e2), e2);
- } else if (e2 instanceof Term) {
- ((Term) e2).setType(newType);
- updatedVars.put(System.identityHashCode(e2), e2);
+ Map.Entry, Type> typeAndExps = msgTypeMap.get(i);
+ if (typeAndExps == null) {
+ List exps = new ArrayList<>();
+ exps.add(arg);
+ typeAndExps = new AbstractMap.SimpleEntry<>(exps, argType);
+ msgTypeMap.put(i, typeAndExps);
+ expToMessage.put(System.identityHashCode(arg), exps);
+ } else {
+ typeAndExps.getKey().add(arg);
+ expToMessage.put(System.identityHashCode(arg), typeAndExps.getKey());
+ Map updateExps = getUpdateSet(updateFromMessage, typeAndExps.getKey());
+ if (compareTypes(typeAndExps.getValue(), argType)) {
+ typeAndExps.setValue(argType);
+ for (Expression e : typeAndExps.getKey()) {
+ if (e != arg) {
+ if (e instanceof Variable) {
+ ((Variable) e).setType(argType);
+ updateExps.put(System.identityHashCode(e), e);
+ }
+ }
+ }
+ } else if (compareTypes(argType, typeAndExps.getValue())) {
+ if (arg instanceof Variable) {
+ ((Variable) arg).setType(typeAndExps.getValue());
+ updateExps.put(System.identityHashCode(arg), arg);
+ } else if (arg instanceof Term) {
+ ((Term) arg).setType(typeAndExps.getValue());
+ updateExps.put(System.identityHashCode(arg), arg);
}
}
- } else {
- if (e instanceof Variable && compareTypes(((Variable) e).getType(), condType)) {
- ((Variable) e).setType(condType);
- updatedVars.put(System.identityHashCode(e), e);
- } else if (e instanceof Term && compareTypes(((Term) e).getType(), condType)) {
- ((Term) e).setType(condType);
- updatedVars.put(System.identityHashCode(e), e);
- }
}
- consExps.add(e);
- expToVariable.put(System.identityHashCode(e), consExps);
}
}
- variables.put(System.identityHashCode(consExps), condType);
+ }
+ for (Channel childCh: ch.getChildren()) {
+ groupForChannel(rootCh, childCh);
}
}
+ };
+ groupExpressionsByMessage.groupForChannel(ch, ch);
+
+ // 1.4 Extract constraints on expressions in each term.
+ IExtractConstraintsOnExpressionsInTerm extractConstraintsOnExpressionsInTerm = new IExtractConstraintsOnExpressionsInTerm() {
+ public void extractForChannel(Channel ch) {
+ for (ChannelMember cm : ch.getChannelMembers()) {
+ StateTransition st = cm.getStateTransition();
+ List terms = new ArrayList<>();
+ if (st.getCurStateExpression() instanceof Term) {
+ Map subTerms = ((Term) st.getCurStateExpression()).getSubTerms(Term.class);
+ terms.addAll(subTerms.values());
+ }
+ if (st.getMessageExpression() instanceof Term) {
+ Map subTerms = ((Term) st.getMessageExpression()).getSubTerms(Term.class);
+ terms.addAll(subTerms.values());
+ }
+ if (st.getNextStateExpression() != null && st.getNextStateExpression() instanceof Term) {
+ Map subTerms = ((Term) st.getNextStateExpression()).getSubTerms(Term.class);
+ terms.addAll(subTerms.values());
+ }
+ for (Term t : terms) {
+ Symbol symbol = t.getSymbol();
+ if (symbol.equals(DataConstraintModel.cons) || symbol.equals(DataConstraintModel.set) || symbol.equals(DataConstraintModel.append)) {
+ // If the root symbol of the term is cons or set.
+ List consExps = new ArrayList<>();
+ consExps.add(t); // list term
+ updateExpressionBelonging(expToConsOrSet, t, consExps);
+ if (symbol.equals(DataConstraintModel.cons)) {
+ // If the root symbol of the term is cons.
+ for (Expression e : t.getChildren()) {
+ consExps.add(e);
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ }
+ } else if (symbol.equals(DataConstraintModel.append)) {
+ // If the root symbol of the term is append.
+ Expression e = t.getChildren().get(1);
+ consExps.add(e); // list element
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ e = t.getChildren().get(0);
+ consExps.add(e); // list argument
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ } else {
+ // If the root symbol of the term is set.
+ Expression e = t.getChildren().get(2);
+ consExps.add(e); // list element
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ e = t.getChildren().get(0);
+ consExps.add(e); // list argument
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ }
+ Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2));
+ if (newType != null) {
+ // If the type of the 2nd argument of cons (1st argument of set/append) is more concrete than the type of the term.
+ t.setType(newType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(t), t);
+ } else {
+ Type arg2Type = null;
+ if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
+ arg2Type = ((Variable) consExps.get(2)).getType();
+ if (compareTypes(arg2Type, t.getType())) {
+ // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append).
+ ((Variable) consExps.get(2)).setType(t.getType());
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ }
+ } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
+ arg2Type = ((Term) consExps.get(2)).getType();
+ if (compareTypes(arg2Type, t.getType())) {
+ // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append).
+ ((Term) consExps.get(2)).setType(t.getType());
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ }
+ }
+ }
+ Type newCompType = getExpTypeIfUpdatable(listComponentTypes.get(t.getType()), consExps.get(1));
+ if (newCompType != null) {
+ // If the type of the 1st argument of cons (3rd argument of set) is more concrete than the type of list component.
+ Type newListType = listTypes.get(newCompType);
+ if (newListType == null) {
+ // Create new list type.
+ newListType = createNewListType(newCompType, DataConstraintModel.typeList);
+ }
+ t.setType(newListType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(t), t);
+ if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
+ ((Variable) consExps.get(2)).setType(newListType);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
+ ((Term) consExps.get(2)).setType(newListType);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ }
+ }
+ consOrSet.put(System.identityHashCode(consExps), t.getType());
+ } else if (symbol.equals(DataConstraintModel.head) || symbol.equals(DataConstraintModel.get)) {
+ // If the root symbol of the term is head or get.
+ List consExps = new ArrayList<>();
+ Expression e = t.getChildren().get(0);
+ consExps.add(e); // list argument
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ consExps.add(t); // list's component
+ updateExpressionBelonging(expToConsOrSet, t, consExps);
+ consExps.add(null);
+ Type listType = listTypes.get(t.getType());
+ if (listType == null && t.getType() != null) {
+ // Create a new list type.
+ listType = createNewListType(t.getType(), DataConstraintModel.typeList);
+ }
+ Type newListType = getExpTypeIfUpdatable(listType, consExps.get(0));
+ if (newListType != null) {
+ // If the type of the component of the 1st argument is more concrete than the type of the term.
+ Type newCompType = listComponentTypes.get(newListType);
+ if (newCompType != null) {
+ t.setType(newCompType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(t), t);
+ }
+ consOrSet.put(System.identityHashCode(consExps), newListType);
+ } else {
+ // If the type of the term is more concrete than the type of the component of the 1st argument.
+ if (consExps.get(0) != null && consExps.get(0) instanceof Variable) {
+ ((Variable) consExps.get(0)).setType(listType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0));
+ } else if (consExps.get(0) != null && consExps.get(0) instanceof Term) {
+ ((Term) consExps.get(0)).setType(listType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0));
+ }
+ consOrSet.put(System.identityHashCode(consExps), listType);
+ }
+ } else if (symbol.equals(DataConstraintModel.tail)) {
+ // If the root symbol of the term is tail.
+ List consExps = new ArrayList<>();
+ consExps.add(t); // list term
+ updateExpressionBelonging(expToConsOrSet, t, consExps);
+ consExps.add(null); // list's component
+ Expression e = t.getChildren().get(0);
+ consExps.add(e); // list argument
+ updateExpressionBelonging(expToConsOrSet, e, consExps);
+ Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2));
+ if (newType != null) {
+ // If the type of the argument is more concrete than the type of the term.
+ t.setType(newType);
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(t), t);
+ } else {
+ Type argType = null;
+ if (consExps.get(2) != null && consExps.get(2) instanceof Variable) {
+ argType = ((Variable) consExps.get(2)).getType();
+ if (compareTypes(argType, t.getType())) {
+ // If the type of the term is more concrete than the type of the argument.
+ ((Variable) consExps.get(2)).setType(t.getType());
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ }
+ } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) {
+ argType = ((Term) consExps.get(2)).getType();
+ if (compareTypes(argType, t.getType())) {
+ // If the type of the term is more concrete than the type of the argument.
+ ((Term) consExps.get(2)).setType(t.getType());
+ Map updateCons = getUpdateSet(updateFromConsOrSet, consExps);
+ updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2));
+ }
+ }
+ }
+ consOrSet.put(System.identityHashCode(consExps), t.getType());
+ } else if (symbol.equals(DataConstraintModel.tuple)) {
+ // If the root symbol of the term is tuple.
+ List tupleExps = new ArrayList<>();
+ List newArgTypesList = new ArrayList<>();
+ tupleExps.add(t); // tuple term
+ updateExpressionBelonging(expToTuple, t, tupleExps);
+ for (Expression e : t.getChildren()) {
+ tupleExps.add(e); // tuple's component
+ updateExpressionBelonging(expToTuple, e, tupleExps);
+ if (e instanceof Variable) {
+ newArgTypesList.add(((Variable) e).getType());
+ } else if (e instanceof Term) {
+ newArgTypesList.add(((Term) e).getType());
+ } else {
+ newArgTypesList.add(null);
+ }
+ }
+ if (t.getType() == DataConstraintModel.typeTuple) {
+ Type newTupleType = tupleTypes.get(newArgTypesList);
+ if (newTupleType == null) {
+ // Create new tuple type;
+ newTupleType = createNewTupleType(newArgTypesList, DataConstraintModel.typeTuple);
+ }
+ // Update the type of the tuple term and record the updated expression.
+ t.setType(newTupleType);
+ Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
+ updateExps.put(System.identityHashCode(t), t);
+ }
+ tuple.put(System.identityHashCode(tupleExps), t.getType());
+ } else if (symbol.equals(DataConstraintModel.pair)) {
+ // If the root symbol of the term is pair.
+ List pairExps = new ArrayList<>();
+ pairExps.add(t); // pair
+ updateExpressionBelonging(expToPair, t, pairExps);
+ if (t.getType() == DataConstraintModel.typePair) {
+ for (Expression e : t.getChildren()) {
+ pairExps.add(e); // left/right
+ updateExpressionBelonging(expToPair, e, pairExps);
+ Type newArgType = null;
+ if (e instanceof Variable) {
+ newArgType = (((Variable) e).getType());
+
+ } else if (e instanceof Term) {
+ newArgType = (((Term) e).getType());
+ }
+
+ if (newArgType != null) {
+ Type newPairType = pairTypes.get(newArgType);
+ if (newPairType != null) {
+ t.setType(newPairType);
+ Map updateExps = getUpdateSet(updateFromPair, pairExps);
+ updateExps.put(System.identityHashCode(t), t);
+ }
+ }
+ }
+ pair.put(System.identityHashCode(pairExps), t.getType());
+
+ }
+ } else if (symbol.equals(DataConstraintModel.fst)) {
+ // If the root symbol of the term is fst.
+ List tupleExps = new ArrayList<>();
+ Expression arg = t.getChildren().get(0);
+ tupleExps.add(arg); // tuple argument
+ updateExpressionBelonging(expToTuple, arg, tupleExps);
+ tupleExps.add(t); // first component
+ updateExpressionBelonging(expToTuple, t, tupleExps);
+ tupleExps.add(null); // second component
+ Type argType = null;
+ if (arg instanceof Variable) {
+ argType = ((Variable) arg).getType();
+ } else if (arg instanceof Term) {
+ argType = ((Term) arg).getType();
+ }
+ Type newTupleType = DataConstraintModel.typeTuple;
+ if (argType == DataConstraintModel.typeTuple && t.getType() != null) {
+ List newCompTypeList = new ArrayList<>();
+ newCompTypeList.add(t.getType());
+ newCompTypeList.add(null);
+ newTupleType = tupleTypes.get(newCompTypeList);
+ if (newTupleType == null) {
+ // Create new tuple type;
+ newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple);
+ }
+ }
+ if (argType != newTupleType && newTupleType != null) {
+ // Update the type of the tuple argument and record the updated expression.
+ if (arg instanceof Variable) {
+ ((Variable) arg).setType(newTupleType);
+ argType = newTupleType;
+ } else if (arg instanceof Term) {
+ ((Term) arg).setType(newTupleType);
+ argType = newTupleType;
+ }
+ Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
+ updateExps.put(System.identityHashCode(arg), arg);
+ }
+ tuple.put(System.identityHashCode(tupleExps), argType);
+ } else if (symbol.equals(DataConstraintModel.snd)) {
+ // If the root symbol of the term is snd.
+ List tupleExps = new ArrayList<>();
+ Expression arg = t.getChildren().get(0);
+ tupleExps.add(arg); // tuple argument
+ updateExpressionBelonging(expToTuple, arg, tupleExps);
+ tupleExps.add(null); // first component
+ tupleExps.add(t); // second component
+ updateExpressionBelonging(expToTuple, t, tupleExps);
+ Type argType = null;
+ if (arg instanceof Variable) {
+ argType = ((Variable) arg).getType();
+ } else if (arg instanceof Term) {
+ argType = ((Term) arg).getType();
+ }
+ Type newTupleType = DataConstraintModel.typeTuple;
+ if (argType == DataConstraintModel.typeTuple && t.getType() != null) {
+ List newCompTypeList = new ArrayList<>();
+ newCompTypeList.add(null);
+ if (DataConstraintModel.typeTuple.isAncestorOf(t.getType())) {
+ List sndTypes = tupleComponentTypes.get(t.getType());
+ if (sndTypes != null) {
+ for (Type t2: sndTypes) {
+ newCompTypeList.add(t2);
+ }
+ } else {
+ newCompTypeList.add(t.getType());
+ }
+ } else {
+ newCompTypeList.add(t.getType());
+ }
+ newTupleType = tupleTypes.get(newCompTypeList);
+ if (newTupleType == null) {
+ // Create new tuple type;
+ newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple);
+ }
+ }
+ if (argType != newTupleType && newTupleType != null) {
+ // Update the type of the tuple argument and record the updated expression.
+ if (arg instanceof Variable) {
+ ((Variable) arg).setType(newTupleType);
+ argType = newTupleType;
+ } else if (arg instanceof Term) {
+ ((Term) arg).setType(newTupleType);
+ argType = newTupleType;
+ }
+ Map updateExps = getUpdateSet(updateFromTuple, tupleExps);
+ updateExps.put(System.identityHashCode(arg), arg);
+ }
+ tuple.put(System.identityHashCode(tupleExps), argType);
+ } else if (symbol.equals(DataConstraintModel.left)) {
+ // If the root symbol of the term is left.
+ List pairExps = new ArrayList<>();
+ Expression arg = t.getChildren().get(0);
+ pairExps.add(arg); // pair
+ updateExpressionBelonging(expToPair, arg, pairExps);
+ pairExps.add(t); // left
+ updateExpressionBelonging(expToPair, t, pairExps);
+ pairExps.add(null); // right
+ Type argType = null;
+ if (arg instanceof Variable) {
+ argType = ((Variable) arg).getType();
+ } else if (arg instanceof Term) {
+ argType = ((Term) arg).getType();
+ }
+ Type newPairType = DataConstraintModel.typePair;
+ if (argType == DataConstraintModel.typePair && t.getType() != null) {
+ List newCompTypeList = new ArrayList<>();
+ newCompTypeList.add(t.getType());
+ newCompTypeList.add(null);
+ newPairType = pairTypes.get(newCompTypeList);
+ if (newPairType == null) {
+ // Create new tuple type;
+ newPairType = createNewTupleType(newCompTypeList, DataConstraintModel.typePair);
+ }
+ }
+ if (argType != newPairType && newPairType != null) {
+ if (arg instanceof Variable) {
+ ((Variable) arg).setType(newPairType);
+ argType = newPairType;
+ } else if (arg instanceof Term) {
+ ((Term) arg).setType(newPairType);
+ argType = newPairType;
+ }
+ Map updateExps = getUpdateSet(updateFromPair, pairExps);
+ updateExps.put(System.identityHashCode(arg), arg);
+ }
+ pair.put(System.identityHashCode(pairExps), argType);
+ } else if (symbol.equals(DataConstraintModel.right)) {
+ // If the root symbol of the term is right.
+ List pairExps = new ArrayList<>();
+ Expression arg = t.getChildren().get(0);
+ pairExps.add(arg); // pair
+ updateExpressionBelonging(expToPair, arg, pairExps);
+ pairExps.add(null); // left
+ pairExps.add(t); // right
+ updateExpressionBelonging(expToPair, t, pairExps);
+ Type argType = null;
+ if (arg instanceof Variable) {
+ argType = ((Variable) arg).getType();
+ } else if (arg instanceof Term) {
+ argType = ((Term) arg).getType();
+ }
+ Type newPairType = DataConstraintModel.typePair;
+ if (argType == DataConstraintModel.typePair && t.getType() != null) {
+ List newCompTypeList = new ArrayList<>();
+ newCompTypeList.add(null);
+ newCompTypeList.add(t.getType());
+ newPairType = pairTypes.get(newCompTypeList);
+ if (newPairType == null) {
+ // Create new tuple type;
+ newPairType = createNewTupleType(newCompTypeList, DataConstraintModel.typePair);
+ }
+ }
+ if (argType != newPairType && newPairType != null) {
+ if (arg instanceof Variable) {
+ ((Variable) arg).setType(newPairType);
+ argType = newPairType;
+ } else if (arg instanceof Term) {
+ ((Term) arg).setType(newPairType);
+ argType = newPairType;
+ }
+ Map updateExps = getUpdateSet(updateFromPair, pairExps);
+ updateExps.put(System.identityHashCode(arg), arg);
+ }
+ pair.put(System.identityHashCode(pairExps), argType);
+ } else if (symbol.equals(DataConstraintModel.lookup)) {
+ // If the root symbol of the term is lookup.
+ List mapExps = new ArrayList<>();
+ Expression arg1 = t.getChildren().get(0); // map
+ mapExps.add(arg1);
+ updateExpressionBelonging(expToMap, arg1, mapExps);
+ Expression arg2 = t.getChildren().get(1); // key
+ mapExps.add(arg2);
+ updateExpressionBelonging(expToMap, arg2, mapExps);
+ mapExps.add(t); // value
+ updateExpressionBelonging(expToMap, t, mapExps);
+ Type arg1Type = null;
+ if (arg1 instanceof Variable) {
+ arg1Type = ((Variable) arg1).getType();
+ } else if (arg1 instanceof Term) {
+ arg1Type = ((Term) arg1).getType();
+ }
+ List newCompTypeList = new ArrayList<>();
+ if (arg2 instanceof Variable) {
+ newCompTypeList.add(((Variable) arg2).getType());
+ } else if (arg2 instanceof Term) {
+ newCompTypeList.add(((Term) arg2).getType());
+ } else {
+ newCompTypeList.add(null);
+ }
+ newCompTypeList.add(t.getType());
+ if (arg1Type == DataConstraintModel.typeMap || arg1Type == null) {
+ Type newMapType = mapTypes.get(newCompTypeList);
+ if (newMapType == null) {
+ // Create new tuple type;
+ newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap);
+ }
+ // Update the type of the map argument and record the updated expression.
+ if (arg1 instanceof Variable) {
+ ((Variable) arg1).setType(newMapType);
+ arg1Type = newMapType;
+ } else if (arg1 instanceof Term) {
+ ((Term) arg1).setType(newMapType);
+ arg1Type = newMapType;
+ }
+ Map updateExps = getUpdateSet(updateFromMap, mapExps);
+ updateExps.put(System.identityHashCode(arg1), arg1);
+ }
+ map.put(System.identityHashCode(mapExps), arg1Type);
+ } else if (symbol.equals(DataConstraintModel.insert)) {
+ // If the root symbol of the term is insert.
+ List mapExps = new ArrayList<>();
+ mapExps.add(t); // map
+ updateExpressionBelonging(expToMap, t, mapExps);
+ Expression arg1 = t.getChildren().get(1); // key
+ mapExps.add(arg1);
+ updateExpressionBelonging(expToMap, arg1, mapExps);
+ Expression arg2 = t.getChildren().get(2); // value
+ mapExps.add(arg2);
+ updateExpressionBelonging(expToMap, arg2, mapExps);
+ Expression arg0 = t.getChildren().get(0); // map
+ mapExps.add(arg0);
+ updateExpressionBelonging(expToMap, arg0, mapExps);
+ Type termType = t.getType();
+ List newCompTypeList = new ArrayList<>();
+ if (arg1 instanceof Variable) {
+ newCompTypeList.add(((Variable) arg1).getType());
+ } else if (arg1 instanceof Term) {
+ newCompTypeList.add(((Term) arg1).getType());
+ } else {
+ newCompTypeList.add(null);
+ }
+ if (arg2 instanceof Variable) {
+ newCompTypeList.add(((Variable) arg2).getType());
+ } else if (arg2 instanceof Term) {
+ newCompTypeList.add(((Term) arg2).getType());
+ } else {
+ newCompTypeList.add(null);
+ }
+ Type newTermType = getExpTypeIfUpdatable(termType, mapExps.get(3));
+ if (newTermType != null) {
+ // If the type of the 1st argument of insert is more concrete than the type of the term.
+ t.setType(newTermType);
+ termType = newTermType;
+ Map updateExps = getUpdateSet(updateFromMap, mapExps);
+ updateExps.put(System.identityHashCode(t), t);
+ } else {
+ Type arg3Type = null;
+ if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) {
+ arg3Type = ((Variable) mapExps.get(3)).getType();
+ if (compareTypes(arg3Type, t.getType())) {
+ // If the type of the term is more concrete than the type of the 1st argument of insert.
+ ((Variable) mapExps.get(3)).setType(t.getType());
+ Map updateExps = getUpdateSet(updateFromMap, mapExps);
+ updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3));
+ }
+ } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) {
+ arg3Type = ((Term) mapExps.get(3)).getType();
+ if (compareTypes(arg3Type, t.getType())) {
+ // If the type of the term is more concrete than the type of the 1st argument of insert.
+ ((Term) mapExps.get(3)).setType(t.getType());
+ Map updateExps = getUpdateSet(updateFromMap, mapExps);
+ updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3));
+ }
+ }
+ }
+ if (termType == DataConstraintModel.typeMap || termType == null) {
+ Type newMapType = mapTypes.get(newCompTypeList);
+ if (newMapType == null) {
+ // Create new tuple type;
+ newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap);
+ }
+ // Update the type of the map term and record the updated expression.
+ t.setType(newMapType);
+ Map updateExps = getUpdateSet(updateFromMap, mapExps);
+ updateExps.put(System.identityHashCode(t), t);
+ if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) {
+ ((Variable) mapExps.get(3)).setType(newMapType);
+ updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3));
+ } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) {
+ ((Term) mapExps.get(3)).setType(newMapType);
+ updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3));
+ }
+ termType = newMapType;
+ }
+ map.put(System.identityHashCode(mapExps), termType);
+ } else if (symbol.equals(DataConstraintModel.addMember)) {
+ // If the root symbol of the term is addMember (addMember(json, key, value)).
+ List dotExps = new ArrayList<>();
+ Expression jsonArg = t.getChildren().get(0);
+ Expression keyArg = t.getChildren().get(1);
+ Expression valueArg = t.getChildren().get(2);
+ dotExps.add(t); // json
+ updateExpressionBelonging(expToJson, t, dotExps);
+ dotExps.add(keyArg); // key
+ updateExpressionBelonging(expToJson, keyArg, dotExps);
+ dotExps.add(valueArg); // value
+ updateExpressionBelonging(expToJson, valueArg, dotExps);
+ dotExps.add(jsonArg); // json
+ updateExpressionBelonging(expToJson, jsonArg, dotExps);
+ Type jsonType = t.getType();
+ Type valueType = null;
+ if (valueArg instanceof Variable) {
+ valueType = ((Variable) valueArg).getType();
+ } else if (valueArg instanceof Term) {
+ valueType = ((Term) valueArg).getType();
+ }
+ String keyName = null;
+ if (keyArg instanceof Constant) {
+ keyName = ((Constant) keyArg).getSymbol().getName();
+ }
+ Type jsonArgType = null;
+ if (jsonArg instanceof Variable) {
+ jsonArgType = ((Variable) jsonArg).getType();
+ } else if (jsonArg instanceof Term) {
+ jsonArgType = ((Term) jsonArg).getType();
+ }
+ Type newJsonType = DataConstraintModel.typeJson;
+ if (jsonType == DataConstraintModel.typeJson && jsonArgType != null && keyName != null) {
+ Map newMemberTypes = new HashMap<>(((JsonType) jsonArgType).getMemberTypes());
+ newMemberTypes.put(keyName, valueType);
+ newJsonType = jsonTypes.get(newMemberTypes);
+ if (newJsonType == null) {
+ // Create new json type;
+ newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson);
+ }
+ }
+ if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) {
+ // Update the type of the json term and record the updated expression.
+ t.setType(newJsonType);
+ jsonType = newJsonType;
+ Map updateExps = getUpdateSet(updateFromJson, dotExps);
+ updateExps.put(System.identityHashCode(t), t);
+ }
+ json.put(System.identityHashCode(dotExps), jsonType);
+ } else if (symbol.equals(DataConstraintModel.dot)) {
+ // If the root symbol of the term is dot (json.property).
+ List dotExps = new ArrayList<>();
+ Expression jsonArg = t.getChildren().get(0);
+ Expression keyArg = t.getChildren().get(1);
+ dotExps.add(jsonArg); // json
+ updateExpressionBelonging(expToJson, jsonArg, dotExps);
+ dotExps.add(keyArg); // key
+ updateExpressionBelonging(expToJson, keyArg, dotExps);
+ dotExps.add(t); // value
+ updateExpressionBelonging(expToJson, t, dotExps);
+ dotExps.add(null); // json
+ Type jsonType = null;
+ if (jsonArg instanceof Variable) {
+ jsonType = ((Variable) jsonArg).getType();
+ } else if (jsonArg instanceof Term) {
+ jsonType = ((Term) jsonArg).getType();
+ }
+ String keyName = null;
+ if (keyArg instanceof Constant) {
+ keyName = ((Constant) keyArg).getSymbol().getName();
+ }
+ Type newJsonType = DataConstraintModel.typeJson;
+ if (jsonType == DataConstraintModel.typeJson && t.getType() != null && keyName != null) {
+ Map newMemberTypes = new HashMap<>();
+ newMemberTypes.put(keyName, t.getType());
+ newJsonType = jsonTypes.get(newMemberTypes);
+ if (newJsonType == null) {
+ // Create new json type;
+ newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson);
+ }
+ }
+ if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) {
+ // Update the type of the json argument and record the updated expression.
+ if (jsonArg instanceof Variable) {
+ ((Variable) jsonArg).setType(newJsonType);
+ jsonType = newJsonType;
+ } else if (jsonArg instanceof Term) {
+ ((Term) jsonArg).setType(newJsonType);
+ jsonType = newJsonType;
+ }
+ Map updateExps = getUpdateSet(updateFromJson, dotExps);
+ updateExps.put(System.identityHashCode(jsonArg), jsonArg);
+ }
+ json.put(System.identityHashCode(dotExps), jsonType);
+ } else if (symbol.equals(DataConstraintModel.dotParam)) {
+ // If the root symbol of the term is dot (json.{param}).
+ List dotExps = new ArrayList<>();
+ Expression jsonArg = t.getChildren().get(0);
+ Expression keyArg = t.getChildren().get(1);
+ dotExps.add(jsonArg); // json (list/map)
+ updateExpressionBelonging(expToJson, jsonArg, dotExps);
+ dotExps.add(null); // key
+ dotExps.add(t); // value
+ updateExpressionBelonging(expToJson, t, dotExps);
+ dotExps.add(null); // json
+ Type jsonType = null;
+ if (jsonArg instanceof Variable) {
+ jsonType = ((Variable) jsonArg).getType();
+ } else if (jsonArg instanceof Term) {
+ jsonType = ((Term) jsonArg).getType();
+ }
+ Type keyType = null;
+ if (keyArg instanceof Variable) {
+ keyType = ((Variable) keyArg).getType();
+ } else if (keyArg instanceof Term) {
+ keyType = ((Term) keyArg).getType();
+ }
+ Type newJsonType = null;
+ if (keyType == DataConstraintModel.typeInt) {
+ newJsonType = DataConstraintModel.typeList;
+ } else if (keyType == DataConstraintModel.typeString) {
+ newJsonType = DataConstraintModel.typeMap;
+ }
+ if (t.getType() != null) {
+ if ((jsonType == DataConstraintModel.typeList)) {
+ newJsonType = listTypes.get(t.getType());
+ if (newJsonType == null) {
+ // Create new list type;
+ newJsonType = createNewListType(t.getType(), DataConstraintModel.typeList);
+ }
+ } else if (jsonType == DataConstraintModel.typeMap) {
+ List keyValueTypes = Arrays.asList(new Type[] {DataConstraintModel.typeString, t.getType()});
+ newJsonType = mapTypes.get(keyValueTypes);
+ if (newJsonType == null) {
+ // Create new map type;
+ newJsonType = createNewMapType(keyValueTypes, DataConstraintModel.typeMap);
+ }
+ }
+ }
+ if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) {
+ // Update the type of the json argument and record the updated expression.
+ if (jsonArg instanceof Variable) {
+ ((Variable) jsonArg).setType(newJsonType);
+ jsonType = newJsonType;
+ } else if (jsonArg instanceof Term) {
+ ((Term) jsonArg).setType(newJsonType);
+ jsonType = newJsonType;
+ }
+ Map updateExps = getUpdateSet(updateFromJson, dotExps);
+ updateExps.put(System.identityHashCode(jsonArg), jsonArg);
+ }
+ json.put(System.identityHashCode(dotExps), jsonType);
+ } else if (symbol.equals(DataConstraintModel.cond)) {
+ // If the root symbol of the term is if function.
+ Expression c1 = t.getChild(1);
+ Expression c2 = t.getChild(2);
+ List condTerms = new ArrayList<>();
+ condTerms.add(t);
+ condTerms.add(c1);
+ condTerms.add(c2);
+ expToVariable.put(System.identityHashCode(t), condTerms);
+ expToVariable.put(System.identityHashCode(c1), condTerms);
+ expToVariable.put(System.identityHashCode(c2), condTerms);
+ Type condType = t.getType();
+ Map updatedVars = getUpdateSet(updateFromVariable, condTerms);
+ Type child1Type = getExpTypeIfUpdatable(condType, c1);
+ if (child1Type != null) {
+ condType = child1Type;
+ t.setType(child1Type);
+ updatedVars.put(System.identityHashCode(t), t);
+ } else {
+ if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), condType)) {
+ ((Variable) c1).setType(condType);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), condType)) {
+ ((Term) c1).setType(condType);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ }
+ }
+ Type child2Type = getExpTypeIfUpdatable(condType, c2);
+ if (child2Type != null) {
+ condType = child2Type;
+ t.setType(child2Type);
+ updatedVars.put(System.identityHashCode(t), t);
+ if (c1 instanceof Variable) {
+ ((Variable) c1).setType(child2Type);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ } else if (c1 instanceof Term) {
+ ((Term) c1).setType(child2Type);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ }
+ } else {
+ if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), condType)) {
+ ((Variable) c2).setType(condType);
+ updatedVars.put(System.identityHashCode(c2), c2);
+ } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), condType)) {
+ ((Term) c2).setType(condType);
+ updatedVars.put(System.identityHashCode(c2), c2);
+ }
+ }
+ variables.put(System.identityHashCode(condTerms), condType);
+ } else if (symbol.equals(DataConstraintModel.add) || symbol.equals(DataConstraintModel.sub)
+ || symbol.equals(DataConstraintModel.mul) || symbol.equals(DataConstraintModel.div)) {
+ // If the root symbol of the term is arithmetic operators.
+ Expression c1 = t.getChild(0);
+ Expression c2 = t.getChild(1);
+ List operands = new ArrayList<>();
+ operands.add(t);
+ operands.add(c1);
+ operands.add(c2);
+ expToVariable.put(System.identityHashCode(t), operands);
+ expToVariable.put(System.identityHashCode(c1), operands);
+ expToVariable.put(System.identityHashCode(c2), operands);
+ Type opType = t.getType();
+ Map updatedVars = getUpdateSet(updateFromVariable, operands);
+ Type child1Type = getExpTypeIfUpdatable(opType, c1);
+ if (child1Type != null) {
+ opType = child1Type;
+ t.setType(child1Type);
+ updatedVars.put(System.identityHashCode(t), t);
+ } else {
+ if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), opType)) {
+ ((Variable) c1).setType(opType);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), opType)) {
+ ((Term) c1).setType(opType);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ }
+ }
+ Type child2Type = getExpTypeIfUpdatable(opType, c2);
+ if (child2Type != null) {
+ opType = child2Type;
+ t.setType(child2Type);
+ updatedVars.put(System.identityHashCode(t), t);
+ if (c1 instanceof Variable) {
+ ((Variable) c1).setType(child2Type);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ } else if (c1 instanceof Term) {
+ ((Term) c1).setType(child2Type);
+ updatedVars.put(System.identityHashCode(c1), c1);
+ }
+ } else {
+ if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), opType)) {
+ ((Variable) c2).setType(opType);
+ updatedVars.put(System.identityHashCode(c2), c2);
+ } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), opType)) {
+ ((Term) c2).setType(opType);
+ updatedVars.put(System.identityHashCode(c2), c2);
+ }
+ }
+ variables.put(System.identityHashCode(operands), opType);
+ } else if (symbol.getSignature() != null
+ && symbol.getSignature()[0] == DataConstraintModel.typeList) {
+ // If the root symbol of the term is the list type (except for the cons function).
+ List consExps = new ArrayList<>();
+ consExps.add(t);
+ expToVariable.put(System.identityHashCode(t), consExps);
+ Type condType = t.getType();
+ Map updatedVars = getUpdateSet(updateFromVariable, consExps);
+ for (int i = 1; i < symbol.getSignature().length; i++) {
+ Type tc = symbol.getSignature()[i];
+ if (tc == DataConstraintModel.typeList) {
+ Expression e = t.getChildren().get(i - 1);
+ Type newType = getExpTypeIfUpdatable(condType, e);
+ if (newType != null) {
+ condType = newType;
+ for (Expression e2 : consExps) {
+ if (e2 instanceof Variable) {
+ ((Variable) e2).setType(newType);
+ updatedVars.put(System.identityHashCode(e2), e2);
+ } else if (e2 instanceof Term) {
+ ((Term) e2).setType(newType);
+ updatedVars.put(System.identityHashCode(e2), e2);
+ }
+ }
+ } else {
+ if (e instanceof Variable && compareTypes(((Variable) e).getType(), condType)) {
+ ((Variable) e).setType(condType);
+ updatedVars.put(System.identityHashCode(e), e);
+ } else if (e instanceof Term && compareTypes(((Term) e).getType(), condType)) {
+ ((Term) e).setType(condType);
+ updatedVars.put(System.identityHashCode(e), e);
+ }
+ }
+ consExps.add(e);
+ expToVariable.put(System.identityHashCode(e), consExps);
+ }
+ }
+ variables.put(System.identityHashCode(consExps), condType);
+ }
+ }
+ }
+ for (Channel childCh: ch.getChildren()) {
+ extractForChannel(childCh);
+ }
+ }
+ };
+ extractConstraintsOnExpressionsInTerm.extractForChannel(ch);
+
+ // 1.5 Extract constraints on path parameters and resources.
+ IExtractConstraintsOnPathParametersAndResources extractConstraintsOnPathParametersAndResources = new IExtractConstraintsOnPathParametersAndResources() {
+ public void extractForChannel(Channel ch) {
+ for (ChannelMember cm : ch.getChannelMembers()) {
+ ResourcePath rPath = cm.getResource();
+ while (rPath != null) {
+ Expression param = rPath.getLastParam();
+ if (param != null) {
+ ResourceHierarchy parent = rPath.getResourceHierarchy().getParent();
+ if (parent != null) {
+ List pathParams = resourcePathParams.get(parent);
+ if (pathParams == null) {
+ pathParams = new ArrayList<>();
+ resourcePathParams.put(parent, pathParams);
+ }
+ pathParams.add(param);
+ expToPathParams.put(System.identityHashCode(param), pathParams);
+ Type parentType = parent.getResourceStateType();
+ Type paramType = null;
+ if (param instanceof Variable) {
+ paramType = ((Variable) param).getType();
+ } else if (param instanceof Term) {
+ paramType = ((Term) param).getType();
+ }
+ if (paramType != null && parentType == null) {
+ if (paramType.equals(DataConstraintModel.typeString)) {
+ parentType = DataConstraintModel.typeMap;
+ } else if (paramType.equals(DataConstraintModel.typeInt)) {
+ parentType = DataConstraintModel.typeList;
+ }
+ if (parentType != null) {
+ parent.setResourceStateType(parentType);
+ updateFromResourceOwnership.add(parent);
+ }
+ }
+ }
+ }
+ rPath = rPath.getParent();
+ }
+ }
+ for (Channel childCh: ch.getChildren()) {
+ extractForChannel(childCh);
+ }
+ }
+ };
+ extractConstraintsOnPathParametersAndResources.extractForChannel(ch);
+ }
+
+ // 1.6 Extract constraints on resource hierarchies.
+ for (ResourceHierarchy res: model.getResourceHierarchies()) {
+ if (res.getResourceStateType() != null) {
+ updateFromResourceOwnership.add(res);
}
}
// 2. Propagate type information.
while (updateFromResource.size() > 0 || updateFromVariable.size() > 0 || updateFromMessage.size() > 0
- || updateFromConsOrSet.size() > 0 || updateFromTuple.size() > 0 || updateFromPair.size() > 0 || updateFromMap.size() > 0) {
+ || updateFromConsOrSet.size() > 0 || updateFromTuple.size() > 0 || updateFromPair.size() > 0
+ || updateFromMap.size() > 0 || updateFromJson.size() > 0 || updateFromResourceOwnership.size() > 0) {
if (updateFromResource.size() > 0) {
Set resourceKeys = updateFromResource.keySet();
Integer resourceKey = resourceKeys.iterator().next();
@@ -943,6 +1274,8 @@
updateTupleTypes(resExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(resExp, pair, expToPair, updateFromPair);
updateMapTypes(resExp, map, expToMap, updateFromMap);
+ updateJsonTypes(resExp, json, expToJson, updateFromJson);
+ updateResourcePathParamsTypes(resExp, resourcePathParams, updateFromResourceOwnership);
}
}
if (updateFromVariable.size() > 0) {
@@ -952,13 +1285,15 @@
updateFromVariable.remove(variableKey);
for (int i : variableValue.keySet()) {
Expression var = variableValue.get(i);
- updateResourceTypes(var, resources, expToResource, updateFromResource);
+ updateResourceTypes(var, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(var, variables, expToVariable, updateFromVariable);
updateMessageTypes(var, messages, expToMessage, updateFromMessage);
updateConsOrSetTypes(var, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(var, tuple, expToTuple, updateFromTuple);
updatePairTypes(var, pair, expToPair, updateFromPair);
updateMapTypes(var, map, expToMap, updateFromMap);
+ updateJsonTypes(var, json, expToJson, updateFromJson);
+ updateResourcePathParamsTypes(var, resourcePathParams, updateFromResourceOwnership);
}
}
if (updateFromMessage.size() > 0) {
@@ -968,12 +1303,14 @@
updateFromMessage.remove(messageKey);
for (int i : messageValue.keySet()) {
Expression mesExp = messageValue.get(i);
- updateResourceTypes(mesExp, resources, expToResource, updateFromResource);
+ updateResourceTypes(mesExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(mesExp, variables, expToVariable, updateFromVariable);
updateConsOrSetTypes(mesExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(mesExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(mesExp, pair, expToPair, updateFromPair);
updateMapTypes(mesExp, map, expToMap, updateFromMap);
+ updateJsonTypes(mesExp, json, expToJson, updateFromJson);
+ updateResourcePathParamsTypes(mesExp, resourcePathParams, updateFromResourceOwnership);
}
}
if (updateFromConsOrSet.size() > 0) {
@@ -983,13 +1320,14 @@
updateFromConsOrSet.remove(consKey);
for (int i : consValue.keySet()) {
Expression consExp = consValue.get(i);
- updateResourceTypes(consExp, resources, expToResource, updateFromResource);
+ updateResourceTypes(consExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(consExp, variables, expToVariable, updateFromVariable);
updateMessageTypes(consExp, messages, expToMessage, updateFromMessage);
updateConsOrSetTypes(consExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(consExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(consExp, pair, expToPair, updateFromPair);
updateMapTypes(consExp, map, expToMap, updateFromMap);
+ updateJsonTypes(consExp, json, expToJson, updateFromJson);
}
}
if (updateFromTuple.size() > 0) {
@@ -999,13 +1337,14 @@
updateFromTuple.remove(tupleKey);
for (int i : tupleValue.keySet()) {
Expression tupleExp = tupleValue.get(i);
- updateResourceTypes(tupleExp, resources, expToResource, updateFromResource);
+ updateResourceTypes(tupleExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(tupleExp, variables, expToVariable, updateFromVariable);
updateMessageTypes(tupleExp, messages, expToMessage, updateFromMessage);
updateConsOrSetTypes(tupleExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(tupleExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(tupleExp, pair, expToPair, updateFromPair);
updateMapTypes(tupleExp, map, expToMap, updateFromMap);
+ updateJsonTypes(tupleExp, json, expToJson, updateFromJson);
}
}
if (updateFromPair.size() > 0) {
@@ -1015,13 +1354,14 @@
updateFromPair.remove(pairKey);
for (int i : pairValue.keySet()) {
Expression pairExp = pairValue.get(i);
- updateResourceTypes(pairExp, resources, expToResource, updateFromResource);
+ updateResourceTypes(pairExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(pairExp, variables, expToVariable, updateFromVariable);
updateMessageTypes(pairExp, messages, expToMessage, updateFromMessage);
updateConsOrSetTypes(pairExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(pairExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(pairExp, pair, expToPair, updateFromPair);
updateMapTypes(pairExp, map, expToMap, updateFromMap);
+ updateJsonTypes(pairExp, json, expToJson, updateFromJson);
}
}
if (updateFromMap.size() > 0) {
@@ -1031,15 +1371,38 @@
updateFromMap.remove(mapKey);
for (int i : mapValue.keySet()) {
Expression mapExp = mapValue.get(i);
- updateResourceTypes(mapExp, resources, expToResource, updateFromResource);
+ updateResourceTypes(mapExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
updateVaribleTypes(mapExp, variables, expToVariable, updateFromVariable);
updateMessageTypes(mapExp, messages, expToMessage, updateFromMessage);
updateConsOrSetTypes(mapExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
updateTupleTypes(mapExp, tuple, expToTuple, updateFromTuple);
updatePairTypes(mapExp, pair, expToPair, updateFromPair);
updateMapTypes(mapExp, map, expToMap, updateFromMap);
+ updateJsonTypes(mapExp, json, expToJson, updateFromJson);
}
}
+ if (updateFromJson.size() > 0) {
+ Set jsonKeys = updateFromJson.keySet();
+ Integer jsonKey = jsonKeys.iterator().next();
+ Map jsonValue = updateFromJson.get(jsonKey);
+ updateFromJson.remove(jsonKey);
+ for (int i : jsonValue.keySet()) {
+ Expression jsonExp = jsonValue.get(i);
+ updateResourceTypes(jsonExp, resources, expToResource, updateFromResource, updateFromResourceOwnership);
+ updateVaribleTypes(jsonExp, variables, expToVariable, updateFromVariable);
+ updateMessageTypes(jsonExp, messages, expToMessage, updateFromMessage);
+ updateConsOrSetTypes(jsonExp, consOrSet, expToConsOrSet, updateFromConsOrSet);
+ updateTupleTypes(jsonExp, tuple, expToTuple, updateFromTuple);
+ updatePairTypes(jsonExp, pair, expToPair, updateFromPair);
+ updateMapTypes(jsonExp, map, expToMap, updateFromMap);
+ updateJsonTypes(jsonExp, json, expToJson, updateFromJson);
+ }
+ }
+ if (updateFromResourceOwnership.size() > 0) {
+ ResourceHierarchy res = updateFromResourceOwnership.iterator().next();
+ updateFromResourceOwnership.remove(res);
+ updateResourceOwnershipTypes(res, resources, expToResource, updateFromResource, updateFromResourceOwnership);
+ }
}
}
@@ -1056,18 +1419,20 @@
}
}
- private static void updateResourceTypes(Expression exp, Map> resources,
- Map> expToResource, Map> updateFromResource) {
- List sameResource = expToResource.get(System.identityHashCode(exp));
- if (sameResource == null) return;
- for (ResourcePath id : resources.keySet()) {
- if (resources.get(id) == sameResource) {
- Type resType = id.getResourceStateType();
+ private static void updateResourceTypes(Expression exp, Map> resources, Map> expToResource,
+ Map> updateFromResource, Set updateFromResourceOwnership) {
+ List identicalResources = expToResource.get(System.identityHashCode(exp));
+ if (identicalResources == null) return;
+ for (ResourceHierarchy res: resources.keySet()) {
+ if (resources.get(res) == identicalResources) {
+ Type resType = res.getResourceStateType();
Type newResType = getExpTypeIfUpdatable(resType, exp);
if (newResType != null) {
- id.setResourceStateType(newResType);
- Map updateExps = getUpdateSet(updateFromResource, sameResource);
- for (Expression resExp : sameResource) {
+ res.setResourceStateType(newResType);
+ updateFromResourceOwnership.add(res); // To update parent and children resources
+ // Update identical resources
+ Map updateExps = getUpdateSet(updateFromResource, identicalResources);
+ for (Expression resExp : identicalResources) {
if (resExp != exp) {
if (resExp instanceof Variable) {
((Variable) resExp).setType(newResType);
@@ -1082,6 +1447,145 @@
}
}
}
+
+ private static void updateResourcePathParamsTypes(Expression exp, Map> resourcePathParams, Set updateFromResourceOwnership) {
+ for (ResourceHierarchy parent: resourcePathParams.keySet()) {
+ List pathParams = resourcePathParams.get(parent);
+ if (pathParams.contains(exp)) {
+ Type parentType = parent.getResourceStateType();
+ Type paramType = null;
+ if (exp instanceof Variable) {
+ paramType = ((Variable) exp).getType();
+ } else if (exp instanceof Term) {
+ paramType = ((Term) exp).getType();
+ }
+ if (paramType != null && parentType == null) {
+ if (paramType.equals(DataConstraintModel.typeString)) {
+ parentType = DataConstraintModel.typeMap;
+ } else if (paramType.equals(DataConstraintModel.typeInt)) {
+ parentType = DataConstraintModel.typeList;
+ }
+ if (parentType != null) {
+ parent.setResourceStateType(parentType);
+ updateFromResourceOwnership.add(parent);
+ }
+ }
+ }
+ }
+ }
+
+ private static void updateResourceOwnershipTypes(ResourceHierarchy res, Map> resources,
+ Map> expToResource, Map> updateFromResource, Set updateFromResourceOwnership) {
+ for (ResourceHierarchy parent: resources.keySet()) {
+ Type resType = res.getResourceStateType();
+ Set children = parent.getChildren();
+ if (res.equals(parent)) {
+ // Propagate an update of a parent resource type to its children' types.
+ if (DataConstraintModel.typeList.isAncestorOf(resType)) {
+ Type newElementType = listComponentTypes.get(resType);
+ if (newElementType != null && children != null && children.size() == 1) {
+ ResourceHierarchy element = children.iterator().next();
+ Type elementType = element.getResourceStateType();
+ if (compareTypes(elementType, newElementType)) {
+ element.setResourceStateType(newElementType);
+ updateFromResourceOwnership.add(element);
+ }
+ }
+ } else if (DataConstraintModel.typeMap.isAncestorOf(resType)) {
+ List newComponentTypes = mapComponentTypes.get(resType);
+ if (newComponentTypes != null && newComponentTypes.size() == 2 && children != null && children.size() == 1) {
+ ResourceHierarchy value = children.iterator().next();
+ Type valueType = value.getResourceStateType();
+ if (compareTypes(valueType, newComponentTypes.get(1))) {
+ value.setResourceStateType(newComponentTypes.get(1));
+ updateFromResourceOwnership.add(value);
+ }
+ }
+ } else if (DataConstraintModel.typeJson.isAncestorOf(resType)) {
+ Map newMemberTypes = jsonMemberTypes.get(resType);
+ if (newMemberTypes != null && newMemberTypes.size() > 0 && children != null && children.size() > 0) {
+ for (ResourceHierarchy chlid: children) {
+ String key = chlid.getResourceName();
+ Type memberType = chlid.getResourceStateType();
+ if (compareTypes(memberType, newMemberTypes.get(key))) {
+ chlid.setResourceStateType(newMemberTypes.get(key));
+ updateFromResourceOwnership.add(chlid);
+ }
+ }
+ }
+ }
+ }
+ if (children.contains(res)) {
+ // Propagate an update of a child resource type to its parent's type.
+ Type parentType = parent.getResourceStateType();
+ if (parentType != null && DataConstraintModel.typeList.isAncestorOf(parentType)) {
+ Type oldElementType = listComponentTypes.get(parentType);
+ if (compareTypes(oldElementType, resType)) {
+ Type newListType = listTypes.get(resType);
+ if (newListType == null) {
+ newListType = createNewListType(resType, parentType);
+ }
+ if (newListType != null) {
+ parent.setResourceStateType(newListType);
+ updateFromResourceOwnership.add(parent);
+ }
+ }
+ } else if (parentType != null && DataConstraintModel.typeMap.isAncestorOf(parentType)) {
+ List oldComponentTypes = mapComponentTypes.get(parentType);
+ if (compareTypes(oldComponentTypes.get(1), resType)) {
+ List newComponentTypes = Arrays.asList(new Type[] {DataConstraintModel.typeString, resType});
+ Type newMapType = mapTypes.get(newComponentTypes);
+ if (newMapType == null) {
+ newMapType = createNewMapType(newComponentTypes, parentType);
+ }
+ if (newMapType != null) {
+ parent.setResourceStateType(newMapType);
+ updateFromResourceOwnership.add(parent);
+ }
+ }
+ } else if (parentType != null && DataConstraintModel.typeJson.isAncestorOf(parentType)) {
+ Map oldMemberTypes = jsonMemberTypes.get(parentType);
+ String key= res.getResourceName();
+ if (oldMemberTypes == null || compareTypes(oldMemberTypes.get(key), resType)) {
+ Map newMemberTypes = new HashMap<>();
+ if (oldMemberTypes != null) newMemberTypes.putAll(oldMemberTypes);
+ newMemberTypes.put(key, resType);
+ Type newJsonType = jsonTypes.get(newMemberTypes);
+ if (newJsonType == null) {
+ newJsonType = createNewJsonType(newMemberTypes, parentType);
+ }
+ if (newJsonType != null) {
+ parent.setResourceStateType(newJsonType);
+ updateFromResourceOwnership.add(parent);
+ }
+ }
+ }
+ }
+ }
+ // Propagate an update of the resource to its expressions.
+ List identicalResources = resources.get(res);
+ if (identicalResources != null) {
+ Type newResType = res.getResourceStateType();
+ for (Expression resExp: identicalResources) {
+ Type resType = null;
+ if (resExp instanceof Variable) {
+ resType = ((Variable) resExp).getType();
+ } else if (resExp instanceof Term) {
+ resType = ((Term) resExp).getType();
+ }
+ if (resType == null || compareTypes(resType, newResType)) {
+ Map updateExps = getUpdateSet(updateFromResource, identicalResources);
+ if (resExp instanceof Variable) {
+ ((Variable) resExp).setType(newResType);
+ updateExps.put(System.identityHashCode(resExp), resExp);
+ } else if (resExp instanceof Term) {
+ ((Term) resExp).setType(newResType);
+ updateExps.put(System.identityHashCode(resExp), resExp);
+ }
+ }
+ }
+ }
+ }
private static void updateVaribleTypes(Expression exp, Map variables,
Map> expToVariable, Map> updateFromVariable) {
@@ -1167,6 +1671,7 @@
int idx = consOrSetComponentGroup.indexOf(exp);
switch (idx) {
case 0:
+ // exp is a list itself.
if (!(exp instanceof Term)) break;
Type listType = consOrSet.get(System.identityHashCode(consOrSetComponentGroup));
Type expType = getExpTypeIfUpdatable(listType, exp);
@@ -1191,6 +1696,7 @@
}
break;
case 1:
+ // exp is a list's component.
listType = consOrSet.get(System.identityHashCode(consOrSetComponentGroup));
Type compType = listComponentTypes.get(listType);
Type newCompType = getExpTypeIfUpdatable(compType, exp);
@@ -1216,6 +1722,7 @@
}
break;
case 2:
+ // exp is a list itself.
listType = consOrSet.get(System.identityHashCode(consOrSetComponentGroup));
expType = getExpTypeIfUpdatable(listType, exp);
if (expType != null) {
@@ -1245,6 +1752,7 @@
for (List tupleComponentGroup: tupleComponentGroups) {
int idx = tupleComponentGroup.indexOf(exp);
if (idx == 0) {
+ // exp is a tuple itself.
Type tupleType = tuple.get(System.identityHashCode(tupleComponentGroup));
Type newTupleType = getExpTypeIfUpdatable(tupleType, exp);
if (newTupleType != null) {
@@ -1312,6 +1820,7 @@
}
}
} else {
+ // exp is a tuple's component.
Type tupleType = tuple.get(System.identityHashCode(tupleComponentGroup));
List componentTypes = tupleComponentTypes.get(tupleType);
boolean updated = false;
@@ -1382,6 +1891,7 @@
for (List pairComponentGroup: pairComponentGroups) {
int idx = pairComponentGroup.indexOf(exp);
if (idx == 0) {
+ // exp is a pair itself.
Type pairType = pair.get(System.identityHashCode(pairComponentGroup));
Type newPairType = getExpTypeIfUpdatable(pairType, exp);
if (newPairType != null) {
@@ -1405,6 +1915,7 @@
}
}
} else {
+ // exp is a pair's component.
Type pairType = pair.get(System.identityHashCode(pairComponentGroup));
Type compType = pairComponentTypes.get(pairType);
Type newCompType = getExpTypeIfUpdatable(compType, exp);
@@ -1435,6 +1946,7 @@
for (List mapComponentGroup: mapComponentGroups) {
int idx = mapComponentGroup.indexOf(exp);
if (idx == 0 || idx == 3) {
+ // exp is a map itself.
Type mapType = map.get(System.identityHashCode(mapComponentGroup));
Type newMapType = getExpTypeIfUpdatable(mapType, exp);
if (newMapType != null) {
@@ -1478,6 +1990,7 @@
}
}
} else {
+ // exp is a map's key or value.
Type mapType = map.get(System.identityHashCode(mapComponentGroup));
List componentTypes = mapComponentTypes.get(mapType);
Type compType = componentTypes.get(idx - 1);
@@ -1516,6 +2029,118 @@
}
}
+
+ private static void updateJsonTypes(Expression exp, Map json,
+ Map>> expToJson, Map> updateFromJson) {
+ Set> jsonMemberGroups = expToJson.get(System.identityHashCode(exp));
+ if (jsonMemberGroups == null) return;
+ for (List jsonMemberGroup: jsonMemberGroups) {
+ int idx = jsonMemberGroup.indexOf(exp);
+ if (idx == 3) {
+ // exp is a json argument (0:t = addMember(3:json, 1:key, 2:value)).
+ Type jsonType = json.get(System.identityHashCode(jsonMemberGroup));
+ if (jsonType != null && jsonMemberTypes.get(jsonType) != null) {
+ Map memberTypes = new HashMap<>(jsonMemberTypes.get(jsonType));
+ Map argMemberTypes = new HashMap<>(memberTypes);
+ String keyName = null;
+ Type valueType = null;
+ if (jsonMemberGroup.get(1) instanceof Constant) {
+ keyName = ((Constant) jsonMemberGroup.get(1)).getSymbol().getName();
+ valueType = ((Constant) jsonMemberGroup.get(1)).getType();
+ argMemberTypes.remove(keyName);
+ }
+ Type jsonArgType = jsonTypes.get(argMemberTypes);
+ Type newJsonArgType = getExpTypeIfUpdatable(jsonArgType, exp);
+ if (newJsonArgType != null && keyName != null) {
+ // Propagate an update of a json arg's type to its container's (json's) type.
+ argMemberTypes = ((JsonType) newJsonArgType).getMemberTypes();
+ argMemberTypes.put(keyName, valueType);
+ memberTypes.putAll(argMemberTypes);
+ Type newJsonType = jsonTypes.get(memberTypes);
+ if (newJsonType == null) {
+ // Create new json type.
+ newJsonType = createNewJsonType(memberTypes, jsonType);
+ }
+ // Update the type of the json term and record the updated expression.
+ Map updateExps = getUpdateSet(updateFromJson, jsonMemberGroup);
+ Expression jsonExp = jsonMemberGroup.get(0);
+ if (jsonExp instanceof Variable) {
+ ((Variable) jsonExp).setType(newJsonType);
+ updateExps.put(System.identityHashCode(jsonExp), jsonExp);
+ } else if (jsonExp instanceof Term) {
+ ((Term) jsonExp).setType(newJsonType);
+ updateExps.put(System.identityHashCode(jsonExp), jsonExp);
+ }
+ json.put(System.identityHashCode(jsonMemberGroup), newJsonType);
+ }
+ }
+ } else if (idx == 2) {
+ // exp is a value (0:t = addMember(3:json, 1:key, 2:value) or 2:value = dot(0:list/map, 1:key)).
+ Type jsonType = json.get(System.identityHashCode(jsonMemberGroup));
+ Type newJsonType = null;
+ if (exp instanceof Term && ((Term) exp).getSymbol().equals(DataConstraintModel.dotParam)) {
+ if (DataConstraintModel.typeList.isAncestorOf(jsonType)) {
+ Type elementType = listComponentTypes.get(jsonType);
+ Type newElementType = getExpTypeIfUpdatable(elementType, exp);
+ if (newElementType != null) {
+ // Propagate an update of a member's type to its container's (json's) type.
+ newJsonType = listTypes.get(newElementType);
+ if (newJsonType == null) {
+ // Create new json type.
+ newJsonType = createNewListType(newElementType, jsonType);
+ }
+ }
+ } else if (DataConstraintModel.typeMap.isAncestorOf(jsonType)) {
+ List keyValueTypes = mapComponentTypes.get(jsonType);
+ Type newValueType = getExpTypeIfUpdatable(keyValueTypes.get(1), exp);
+ if (newValueType != null) {
+ // Propagate an update of a member's type to its container's (json's) type.
+ List newKeyValueTypes = Arrays.asList(new Type[] {DataConstraintModel.typeString, newValueType});
+ newJsonType = mapTypes.get(newKeyValueTypes);
+ if (newJsonType == null) {
+ // Create new json type.
+ newJsonType = createNewMapType(newKeyValueTypes, jsonType);
+ }
+ }
+ }
+ } else {
+ Map memberTypes = jsonMemberTypes.get(jsonType);
+ String keyName = null;
+ if (jsonMemberGroup.get(1) instanceof Constant) {
+ keyName = ((Constant) jsonMemberGroup.get(1)).getSymbol().getName();
+ }
+ if (memberTypes != null) {
+ Type memberType = memberTypes.get(keyName);
+ Type newMemberType = getExpTypeIfUpdatable(memberType, exp);
+ if (newMemberType != null && keyName != null) {
+ // Propagate an update of a member's type to its container's (json's) type.
+ Map newMemberTypes = new HashMap<>(memberTypes);
+ newMemberTypes.put(keyName, newMemberType);
+ newJsonType = jsonTypes.get(newMemberTypes);
+ if (newJsonType == null) {
+ // Create new json type.
+ newJsonType = createNewJsonType(newMemberTypes, jsonType);
+ }
+ }
+ }
+ }
+ if (newJsonType != null) {
+ // Update the type of the json term and record the updated expression.
+ Map updateExps = getUpdateSet(updateFromJson, jsonMemberGroup);
+ Expression jsonExp = jsonMemberGroup.get(0);
+ if (jsonExp instanceof Variable) {
+ ((Variable) jsonExp).setType(newJsonType);
+ updateExps.put(System.identityHashCode(jsonExp), jsonExp);
+ } else if (jsonExp instanceof Term) {
+ ((Term) jsonExp).setType(newJsonType);
+ updateExps.put(System.identityHashCode(jsonExp), jsonExp);
+ }
+ json.put(System.identityHashCode(jsonMemberGroup), newJsonType);
+ }
+ }
+ }
+ }
+
private static Type createNewListType(Type compType, Type parentType) {
String compTypeName = getInterfaceTypeName(compType);
List childrenTypes = getChildrenTypes(parentType, listComponentTypes.keySet());
@@ -1598,9 +2223,39 @@
return newMapType;
}
- private static List getChildrenTypes(Type parentType, Set componentTypes) {
+ private static JsonType createNewJsonType(Map memberTypes, Type parentJsonType) {
+ String implTypeName = "HashMap<>";
+ String interfaceTypeName = "Map";
+ List childrenTypes = getChildrenTypes(parentJsonType, jsonMemberTypes.keySet());
+ JsonType newJsonType = new JsonType("Json", implTypeName, interfaceTypeName, parentJsonType);
+ for (String key: memberTypes.keySet()) {
+ newJsonType.addMemberType(key, memberTypes.get(key));
+ }
+ jsonTypes.put(memberTypes, newJsonType);
+ jsonMemberTypes.put(newJsonType, memberTypes);
+ for (Type childType : childrenTypes) {
+ if (compareTypes(childType, newJsonType)) {
+ if (newJsonType.getParentTypes().contains(parentJsonType)) {
+ newJsonType.replaceParentType(parentJsonType, childType);
+ } else {
+ newJsonType.addParentType(childType);
+ }
+ } else if (compareTypes(newJsonType, childType)) {
+ childType.replaceParentType(parentJsonType, newJsonType);
+ }
+ }
+ return newJsonType;
+ }
+
+ /**
+ * Get children types of a given type from given set of types.
+ * @param parentType a type
+ * @param allTypes set of types
+ * @return list of the children types
+ */
+ private static List getChildrenTypes(Type parentType, Set allTypes) {
List childrenTypes = new ArrayList<>();
- for (Type childType : componentTypes) {
+ for (Type childType : allTypes) {
if (childType.getParentTypes().contains(parentType)) {
childrenTypes.add(childType);
}
@@ -1626,8 +2281,7 @@
return type.getInterfaceTypeName();
}
- private static > Map getUpdateSet(
- Map> updateSets, U keySet) {
+ private static > Map getUpdateSet(Map> updateSets, U keySet) {
Map updatedExps = updateSets.get(System.identityHashCode(keySet));
if (updatedExps == null) {
updatedExps = new HashMap<>();
@@ -1683,6 +2337,7 @@
for (int i = 0; i < originalCompTypes.size(); i++) {
if (originalCompTypes.get(i) != null) {
if (DataConstraintModel.typeTuple.isAncestorOf(originalCompTypes.get(i))) {
+ // Unfold the nested tuple's types.
Type tupleType = originalCompTypes.remove(i);
for (Type t: tupleComponentTypes.get(tupleType)) {
originalCompTypes.add(t);
@@ -1690,6 +2345,7 @@
}
if (newCompTypes.size() - 1 < i) return false;
if (newCompTypes.get(i) != null && DataConstraintModel.typeTuple.isAncestorOf(newCompTypes.get(i))) {
+ // Unfold the nested tuple's types.
Type tupleType = newCompTypes.remove(i);
for (Type t: tupleComponentTypes.get(tupleType)) {
newCompTypes.add(t);
@@ -1707,7 +2363,40 @@
if (originalCompType != null && (newCompType == null || !originalCompType.isAncestorOf(newCompType))) return false;
return true;
}
+ if (DataConstraintModel.typeJson.isAncestorOf(originalType) && DataConstraintModel.typeJson.isAncestorOf(newType)) {
+ Map originalMemberTypes = jsonMemberTypes.get(originalType);
+ Map newMemberTypes = jsonMemberTypes.get(newType);
+ if (originalMemberTypes == null) return true;
+ if (originalMemberTypes.keySet().size() < newMemberTypes.keySet().size()
+ && newMemberTypes.keySet().containsAll(originalMemberTypes.keySet())) return true;
+ if (originalMemberTypes.keySet().size() > newMemberTypes.keySet().size()) return false;
+ if (!newMemberTypes.keySet().containsAll(originalMemberTypes.keySet())) return false;
+ for (String key: originalMemberTypes.keySet()) {
+ if (!originalMemberTypes.get(key).isAncestorOf(newMemberTypes.get(key))) return false;
+ }
+ return true;
+ }
}
return false;
}
+
+ private static interface IGroupExpressionsByResource {
+ public void groupForChannel(Channel ch);
+ }
+
+ private static interface IGroupExpressionsByVariable {
+ public void groupForChannel(Channel ch);
+ }
+
+ private static interface IGroupExpressionsByMessage {
+ public void groupForChannel(Channel rootCh, Channel ch);
+ }
+
+ private static interface IExtractConstraintsOnExpressionsInTerm {
+ public void extractForChannel(Channel ch);
+ }
+
+ private static interface IExtractConstraintsOnPathParametersAndResources {
+ public void extractForChannel(Channel ch);
+ }
}
diff --git a/AlgebraicDataflowArchitectureModel/src/application/ApplicationMenuBar.java b/AlgebraicDataflowArchitectureModel/src/application/ApplicationMenuBar.java
index 38e2370..1835abf 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/ApplicationMenuBar.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/ApplicationMenuBar.java
@@ -17,6 +17,7 @@
import application.actions.OpenAction;
import application.actions.SaveAction;
import application.actions.SaveAsAction;
+import application.actions.SimulateAction;
import application.actions.TreeLayoutAction;
import application.actions.ZoomInAction;
import application.actions.ZoomOutAction;
@@ -37,6 +38,8 @@
private DAGLayoutAction dagLayoutAction = null;
private TreeLayoutAction treeLayoutAction = null;
private CircleLayoutAction circleLayoutAction = null;
+ //private SimulateAction simulateAction = null;
+
public ApplicationMenuBar(ApplicationWindow applicationWindow) {
this.applicationWindow = applicationWindow;
@@ -72,6 +75,9 @@
menu.add(new ZoomInAction(applicationWindow.getGraphComponent()));
menu.add(new ZoomOutAction(applicationWindow.getGraphComponent()));
+ menu = add(new JMenu("Simulate"));
+ menu.add(new SimulateAction(applicationWindow));
+
menu = add(new JMenu("Generate"));
menu.add(javaPrototypeGenerateAction = new JavaPrototypeGenerateAction(applicationWindow.getEditor()));
menu.add(jerseyPrototypeGenerateAction = new JerseyPrototypeGenerateAction(applicationWindow.getEditor()));
diff --git a/AlgebraicDataflowArchitectureModel/src/application/actions/JavaPrototypeGenerateAction.java b/AlgebraicDataflowArchitectureModel/src/application/actions/JavaPrototypeGenerateAction.java
index 83acc69..4083dce 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/actions/JavaPrototypeGenerateAction.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/actions/JavaPrototypeGenerateAction.java
@@ -13,9 +13,12 @@
import algorithms.*;
import application.editor.Editor;
import code.ast.*;
+import generators.CodeGeneratorFromDataFlowGraph;
import generators.DataTransferMethodAnalyzer;
import generators.JavaCodeGenerator;
import generators.JavaMethodBodyGenerator;
+import generators.JavaSpecific;
+import models.dataConstraintModel.ResourceHierarchy;
import models.dataConstraintModel.ResourcePath;
import models.dataFlowModel.DataTransferModel;
import models.dataFlowModel.ModelExtension;
@@ -45,8 +48,8 @@
if (fileName == null) fileName = "Main";
String mainTypeName = fileName.split("\\.")[0];
boolean exist = false;
- for (ResourcePath id: model.getResourcePaths()) {
- String resourceName = id.getResourceName().substring(0, 1).toUpperCase() + id.getResourceName().substring(1);
+ for (ResourceHierarchy res: model.getResourceHierarchies()) {
+ String resourceName = res.getResourceName().substring(0, 1).toUpperCase() + res.getResourceName().substring(1);
if (mainTypeName.equals(resourceName)) {
exist = true;
}
@@ -57,6 +60,7 @@
JavaCodeGenerator.resetMainTypeName(); // use the default main type's name.
}
editor.setCodes(JavaMethodBodyGenerator.doGenerate(graph, model, JavaCodeGenerator.doGenerate(graph, model)));
+// editor.setCodes(new CodeGeneratorFromDataFlowGraph().generateCode(model, graph, new JavaSpecific()));
ModelExtension.recoverModel(model);
for (CompilationUnit file : editor.getCodes()) {
System.out.println(file);
diff --git a/AlgebraicDataflowArchitectureModel/src/application/actions/JerseyPrototypeGenerateAction.java b/AlgebraicDataflowArchitectureModel/src/application/actions/JerseyPrototypeGenerateAction.java
index 766c384..dbf75fd 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/actions/JerseyPrototypeGenerateAction.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/actions/JerseyPrototypeGenerateAction.java
@@ -17,6 +17,7 @@
import generators.JerseyCodeGenerator;
import generators.JerseyMethodBodyGenerator;
import models.algebra.Type;
+import models.dataConstraintModel.ResourceHierarchy;
import models.dataConstraintModel.ResourcePath;
import models.dataFlowModel.DataTransferModel;
import models.dataFlowModel.ModelExtension;
@@ -46,8 +47,8 @@
if (fileName == null) fileName = "Main";
String mainTypeName = fileName.split("\\.")[0];
boolean exist = false;
- for (ResourcePath id: model.getResourcePaths()) {
- String resourceName = id.getResourceName().substring(0, 1).toUpperCase() + id.getResourceName().substring(1);
+ for (ResourceHierarchy res: model.getResourceHierarchies()) {
+ String resourceName = res.getResourceName().substring(0, 1).toUpperCase() + res.getResourceName().substring(1);
if (mainTypeName.equals(resourceName)) {
exist = true;
}
diff --git a/AlgebraicDataflowArchitectureModel/src/application/actions/NewResourceAction.java b/AlgebraicDataflowArchitectureModel/src/application/actions/NewResourceAction.java
index 50b1512..b01fc46 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/actions/NewResourceAction.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/actions/NewResourceAction.java
@@ -22,7 +22,7 @@
public void actionPerformed(ActionEvent e) {
String resName = JOptionPane.showInputDialog("Resourece Name:");
if (resName == null) return;
- editor.addResourcePath(new ResourcePath(resName, 0));
+ editor.addResourcePath(null, resName);
}
}
diff --git a/AlgebraicDataflowArchitectureModel/src/application/actions/SaveAsAction.java b/AlgebraicDataflowArchitectureModel/src/application/actions/SaveAsAction.java
index 1a38b08..9542cdb 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/actions/SaveAsAction.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/actions/SaveAsAction.java
@@ -65,9 +65,7 @@
lastDir = fc.getSelectedFile().getParent();
String fileName = fc.getSelectedFile().getAbsolutePath() + extension;
-
- // checking file duplicates
- if(! (fc.getSelectedFile().exists())) editor.setCurFilePath(fileName);
+ editor.setCurFilePath(fileName);
// overwriting file
editor.save();
diff --git a/AlgebraicDataflowArchitectureModel/src/application/actions/SimulateAction.java b/AlgebraicDataflowArchitectureModel/src/application/actions/SimulateAction.java
new file mode 100644
index 0000000..26a1779
--- /dev/null
+++ b/AlgebraicDataflowArchitectureModel/src/application/actions/SimulateAction.java
@@ -0,0 +1,38 @@
+package application.actions;
+
+import java.awt.event.ActionEvent;
+import java.io.File;
+
+import javax.swing.JFileChooser;
+import javax.swing.JFrame;
+import javax.swing.JOptionPane;
+import javax.swing.filechooser.FileFilter;
+import javax.swing.filechooser.FileNameExtensionFilter;
+
+import application.ApplicationWindow;
+import application.editor.Editor;
+import application.simulator.SimulatorWindow;
+import models.dataFlowModel.DataTransferChannel;
+
+public class SimulateAction extends AbstractSystemAction {
+
+ private SimulatorWindow simulatorWindow = null;
+
+ /**
+ *
+ */
+ private static final long serialVersionUID = -995609232489316795L;
+
+ public SimulateAction(ApplicationWindow frame) {
+ super("Simulate", frame);
+ //this.simulatorWindow = new SimulatorWindow(frame.getEditor());
+ }
+
+
+ @Override
+ public void actionPerformed(ActionEvent e) {
+ this.simulatorWindow = new SimulatorWindow(frame.getEditor());
+ }
+
+}
+
diff --git a/AlgebraicDataflowArchitectureModel/src/application/editor/DataTransferModelingCellEditor.java b/AlgebraicDataflowArchitectureModel/src/application/editor/DataTransferModelingCellEditor.java
index b4d81a6..f560501 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/editor/DataTransferModelingCellEditor.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/editor/DataTransferModelingCellEditor.java
@@ -30,7 +30,10 @@
import models.visualModel.FormulaChannel;
import parser.Parser;
import parser.Parser.TokenStream;
+import parser.exceptions.ExpectedColon;
+import parser.exceptions.ExpectedDoubleQuotation;
import parser.exceptions.ExpectedRightBracket;
+import parser.exceptions.WrongJsonExpression;
public class DataTransferModelingCellEditor implements mxICellEditor {
public int DEFAULT_MIN_WIDTH = 70;
@@ -67,7 +70,7 @@
DataTransferModel model = editor.getModel();
DataTransferChannel ch = (DataTransferChannel) model.getChannel((String) ((mxCell) cell).getValue());
if (ch == null) {
- ch = (DataTransferChannel) model.getIOChannel((String) ((mxCell) cell).getValue());
+ ch = (DataTransferChannel) model.getInputChannel((String) ((mxCell) cell).getValue());
if(ch == null) {
//resource
return;
@@ -123,7 +126,7 @@
Expression exp = parser.parseTerm(stream, editor.getModel());
((FormulaChannel) ch).setFormula(formula);
((FormulaChannel) ch).setFormulaTerm(exp);
- } catch (ExpectedRightBracket e) {
+ } catch (ExpectedRightBracket | WrongJsonExpression | ExpectedColon | ExpectedDoubleQuotation e) {
e.printStackTrace();
}
}
diff --git a/AlgebraicDataflowArchitectureModel/src/application/editor/Editor.java b/AlgebraicDataflowArchitectureModel/src/application/editor/Editor.java
index b285ce0..c9bfbd5 100644
--- a/AlgebraicDataflowArchitectureModel/src/application/editor/Editor.java
+++ b/AlgebraicDataflowArchitectureModel/src/application/editor/Editor.java
@@ -6,12 +6,16 @@
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
+import java.util.AbstractMap;
+import java.util.AbstractMap.SimpleEntry;
import java.util.ArrayList;
+import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
+import java.util.Map.Entry;
import java.util.Set;
import com.mxgraph.layout.mxCircleLayout;
@@ -19,6 +23,7 @@
import com.mxgraph.model.mxCell;
import com.mxgraph.model.mxGeometry;
import com.mxgraph.model.mxGraphModel;
+import com.mxgraph.model.mxICell;
import com.mxgraph.model.mxIGraphModel;
import com.mxgraph.swing.mxGraphComponent;
import com.mxgraph.util.mxConstants;
@@ -32,15 +37,26 @@
import algorithms.Validation;
import application.layouts.*;
import code.ast.CompilationUnit;
+import generators.JavaCodeGenerator;
import models.Edge;
import models.EdgeAttribute;
import models.Node;
+import models.algebra.Expression;
+import models.algebra.InvalidMessage;
+import models.algebra.ParameterizedIdentifierIsFutureWork;
+import models.algebra.UnificationFailed;
+import models.algebra.ValueUndefined;
import models.dataConstraintModel.Channel;
import models.dataConstraintModel.ChannelMember;
+import models.dataConstraintModel.DataConstraintModel;
+import models.dataConstraintModel.ResourceHierarchy;
import models.dataConstraintModel.ResourcePath;
+import models.dataConstraintModel.Selector;
import models.dataFlowModel.DataTransferModel;
import models.dataFlowModel.DataTransferChannel;
import models.dataFlowModel.PushPullAttribute;
+import models.dataFlowModel.ResolvingMultipleDefinitionIsFutureWork;
+import models.dataFlowModel.ChannelNode;
import models.dataFlowModel.DataFlowEdge;
import models.dataFlowModel.DataFlowGraph;
import models.dataFlowModel.ResourceNode;
@@ -50,10 +66,12 @@
import parser.exceptions.ExpectedAssignment;
import parser.exceptions.ExpectedChannel;
import parser.exceptions.ExpectedChannelName;
+import parser.exceptions.ExpectedColon;
+import parser.exceptions.ExpectedDoubleQuotation;
import parser.exceptions.ExpectedEquals;
import parser.exceptions.ExpectedFormulaChannel;
import parser.exceptions.ExpectedGeometry;
-import parser.exceptions.ExpectedInOrOutOrRefKeyword;
+import parser.exceptions.ExpectedInOrOutOrRefOrSubKeyword;
import parser.exceptions.ExpectedIoChannel;
import parser.exceptions.ExpectedLeftCurlyBracket;
import parser.exceptions.ExpectedModel;
@@ -62,8 +80,11 @@
import parser.exceptions.ExpectedResource;
import parser.exceptions.ExpectedRightBracket;
import parser.exceptions.ExpectedStateTransition;
+import parser.exceptions.WrongJsonExpression;
import parser.exceptions.WrongLHSExpression;
import parser.exceptions.WrongRHSExpression;
+import parser.exceptions.ExpectedRightCurlyBracket;
+import parser.exceptions.WrongPathExpression;
import parser.ParserDTRAM;
public class Editor {
@@ -79,6 +100,8 @@
protected String curFileName = null;
protected String curFilePath = null;
protected ArrayList codes = null;
+
+ private boolean bReflectingArchitectureModel = false;
public Editor(mxGraphComponent graphComponent) {
this.graphComponent = graphComponent;
@@ -105,6 +128,7 @@
public DataFlowGraph getDataFlowGraph() {
if (dataFlowGraph == null) {
analyzeDataTransferModel(getModel());
+ updateEdgeAttiributes(dataFlowGraph);
}
return dataFlowGraph;
}
@@ -112,7 +136,6 @@
public DataFlowGraph analyzeDataTransferModel(DataTransferModel model) {
DataFlowGraph flowGraph = DataTransferModelAnalyzer.createDataFlowGraphWithStateStoringAttribute(model);
dataFlowGraph = DataTransferModelAnalyzer.annotateWithSelectableDataTransferAttiribute(flowGraph);
- updateEdgeAttiributes(dataFlowGraph);
return dataFlowGraph;
}
@@ -175,17 +198,26 @@
} else {
ParserDTRAM parserDTRAM = new ParserDTRAM(new BufferedReader(new FileReader(file)));
try {
+ // Parse the .dtram file.
model = parserDTRAM.doParseModel();
- graph = constructGraph(model);
+
+ // Analyze the model.
+ if (!Validation.checkUpdateConflict(model)) return null;
+ DataFlowGraph dataFlowGraph = analyzeDataTransferModel(model);
+
+ // Visualize the model.
+ graph = constructGraph(model, dataFlowGraph);
parserDTRAM.doParseGeometry(graph);
+ updateEdgeAttiributes(dataFlowGraph);
+
curFilePath = file.getAbsolutePath();
curFileName = file.getName();
- if (!Validation.checkUpdateConflict(model)) return null;
- analyzeDataTransferModel(model);
return model;
- } catch (ExpectedChannel | ExpectedChannelName | ExpectedLeftCurlyBracket | ExpectedInOrOutOrRefKeyword
+ } catch (ExpectedChannel | ExpectedChannelName | ExpectedLeftCurlyBracket | ExpectedInOrOutOrRefOrSubKeyword
| ExpectedStateTransition | ExpectedEquals | ExpectedRHSExpression | WrongLHSExpression
- | WrongRHSExpression | ExpectedRightBracket | ExpectedAssignment | ExpectedModel | ExpectedGeometry | ExpectedNode | ExpectedResource | ExpectedFormulaChannel | ExpectedIoChannel e) {
+ | WrongRHSExpression | ExpectedRightBracket | ExpectedAssignment | ExpectedModel
+ | ExpectedGeometry | ExpectedNode | ExpectedResource | ExpectedFormulaChannel | ExpectedIoChannel
+ | ExpectedRightCurlyBracket | WrongPathExpression | WrongJsonExpression | ExpectedColon | ExpectedDoubleQuotation e) {
e.printStackTrace();
}
}
@@ -205,20 +237,23 @@
// Parse the .model file.
model = parser.doParse();
- curFilePath = file.getAbsolutePath();
- curFileName = file.getName();
-
// Analyze the model.
if (!Validation.checkUpdateConflict(model)) return null;
- graph = constructGraph(model);
- analyzeDataTransferModel(model);
+ DataFlowGraph dataFlowGraph = analyzeDataTransferModel(model);
+
+ // Visualize the model.
+ graph = constructGraph(model, dataFlowGraph);
+ updateEdgeAttiributes(dataFlowGraph);
// Set DAG layout.
- setDAGLayout();
+// setDAGLayout();
+
+ curFilePath = file.getAbsolutePath();
+ curFileName = file.getName();
return model;
- } catch (ExpectedChannel | ExpectedChannelName | ExpectedLeftCurlyBracket | ExpectedInOrOutOrRefKeyword
+ } catch (ExpectedChannel | ExpectedChannelName | ExpectedLeftCurlyBracket | ExpectedInOrOutOrRefOrSubKeyword
| ExpectedStateTransition | ExpectedEquals | ExpectedRHSExpression | WrongLHSExpression
- | WrongRHSExpression | ExpectedRightBracket | ExpectedAssignment e) {
+ | WrongRHSExpression | ExpectedRightBracket | ExpectedAssignment | ExpectedRightCurlyBracket | WrongPathExpression | WrongJsonExpression | ExpectedColon | ExpectedDoubleQuotation e) {
e.printStackTrace();
}
} catch (FileNotFoundException e) {
@@ -303,11 +338,11 @@
}
for (ResourcePath res: model.getResourcePaths()){
- if(res instanceof ResourcePath && state.getLabel().equals(res.getResourceName()))
+ if(res instanceof ResourcePath && state.getLabel().equals(res.getLeafResourceName()))
fileString += "\tnode r " + state.getLabel() + ":" + x + "," + y + "," + w + "," + h + "\n";
}
- for (Channel ioC: model.getIOChannels()) {
+ for (Channel ioC: model.getInputChannels()) {
if(ioC instanceof Channel && state.getLabel().equals(ioC.getChannelName())) {
fileString += "\tnode ioc " + state.getLabel() + ":" + x + "," + y + "," + w + "," + h + "\n";
}
@@ -322,10 +357,11 @@
/**
* Construct a mxGraph from DataFlowModel and DataFlowModel
* @param model
- * @param dataFlowGraph
+ * @param dataFlowGraph
* @return constructed mxGraph
*/
- public mxGraph constructGraph(DataTransferModel model) {
+ public mxGraph constructGraph(DataTransferModel model, DataFlowGraph dataFlowGraph) {
+ bReflectingArchitectureModel = true;
((mxGraphModel) graph.getModel()).clear();
Object parent = graph.getDefaultParent();
graph.getModel().beginUpdate();
@@ -340,69 +376,139 @@
Map channelsIn = new HashMap<>();
Map channelsOut = new HashMap<>();
- Map