diff --git a/bin/.gitignore b/bin/.gitignore new file mode 100644 index 0000000..549e00a --- /dev/null +++ b/bin/.gitignore @@ -0,0 +1,33 @@ +HELP.md +target/ +!.mvn/wrapper/maven-wrapper.jar +!**/src/main/**/target/ +!**/src/test/**/target/ + +### STS ### +.apt_generated +.classpath +.factorypath +.project +.settings +.springBeans +.sts4-cache + +### IntelliJ IDEA ### +.idea +*.iws +*.iml +*.ipr + +### NetBeans ### +/nbproject/private/ +/nbbuild/ +/dist/ +/nbdist/ +/.nb-gradle/ +build/ +!**/src/main/**/build/ +!**/src/test/**/build/ + +### VS Code ### +.vscode/ diff --git a/bin/.mvn/wrapper/maven-wrapper.properties b/bin/.mvn/wrapper/maven-wrapper.properties new file mode 100644 index 0000000..d58dfb7 --- /dev/null +++ b/bin/.mvn/wrapper/maven-wrapper.properties @@ -0,0 +1,19 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. +wrapperVersion=3.3.2 +distributionType=only-script +distributionUrl=https://repo.maven.apache.org/maven2/org/apache/maven/apache-maven/3.9.9/apache-maven-3.9.9-bin.zip diff --git a/bin/models/Accounts.model b/bin/models/Accounts.model new file mode 100644 index 0000000..dba68ba --- /dev/null +++ b/bin/models/Accounts.model @@ -0,0 +1,7 @@ +channel CIO1 { + out accounts(l:Map, signup(id:Int, name:Str)) = append(l, {"name": name}) +} + +channel CIO2(uid:Int) { + out accounts.{uid}.name(n:Str, changeName(name)) = name +} diff --git a/bin/models/Algolike.model b/bin/models/Algolike.model new file mode 100644 index 0000000..8ea8dc2 --- /dev/null +++ b/bin/models/Algolike.model @@ -0,0 +1,113 @@ +init { + deck := nil + handsA := nil + handsB := nil + guessA := 0 + guessB := 0 +} +channel targetAInput{ + out targetA(t:Int, setTargetA(a:Int)) = a +} +channel targetBInput{ + out targetB(t:Int, setTargetB(b:Int)) = b +} +channel attackerAInput{ + out attackerA(t:Int, setAttackerA(a:Int)) = a +} +channel attackerBInput{ + out attackerB(t:Int, setAttackerB(b:Int)) = b +} +channel guessAInput{ + out guessA(t:Int, setGuessA(a:Int)) = a +} +channel guessBInput{ + out guessB(t:Int, setGuessB(b:Int)) = b +} +channel addDeck{ + out deck(d:List, addCard(num:Integer)) = cons(tuple(num, false), d) +} + +channel drawAInput{ + + 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(fst(get(b, t)) == g, t) +} + +channel inputDrawArgsA{ + 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)), + sortByKey(cons(tuple(fst(head(d)), true), outA))) + + 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) +} + +channel selectAInput{ + ref attackerA(a:Int, selectAndAttackA(a, t, g, b)) + 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(fst(get(b, t)) == g, t, a) +} +channel inputSelectArgA{ + 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), + set(outB, fst(snd(sucTrgAtk)), tuple(fst(get(outB, fst(snd(sucTrgAtk)))), true)), + outB) +} +channel drawBInput{ + 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(fst(get(a, t)) == g, t) +} + +channel inputDrawArgsB{ + 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), + 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), + set(outA, snd(sucTrg), tuple(fst(get(outA, snd(sucTrg))), true)), + outA) + out deck(t:List, drawB(sucTrg, d)) = tail(t) +} + +channel selectBInput{ + ref attackerB(atk:Int, selectAndAttackB(atk, t, g, a)) + 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(fst(get(a, t)) == g, t, atk) +} +channel inputSelectArgB{ + 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), + 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)) = length(extractFaceDown(j)) == 0 +} +channel judgeB{ + 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/bin/models/Base.model b/bin/models/Base.model new file mode 100644 index 0000000..bb460e4 --- /dev/null +++ b/bin/models/Base.model @@ -0,0 +1,13 @@ +channel CIO{ + 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 +} +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 +} \ No newline at end of file diff --git a/bin/models/Clock.dtram b/bin/models/Clock.dtram new file mode 100644 index 0000000..bbeb6dc --- /dev/null +++ b/bin/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/bin/models/Clock.model b/bin/models/Clock.model new file mode 100644 index 0000000..0ecb11b --- /dev/null +++ b/bin/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/bin/models/CustomerOffice.model b/bin/models/CustomerOffice.model new file mode 100644 index 0000000..091189a --- /dev/null +++ b/bin/models/CustomerOffice.model @@ -0,0 +1,21 @@ +channel CIO_AddCustomer { + out customers(db:Map, addCustomer(uid:Str, off:Str)) = insert(db, uid, {"off": off}) +} + +channel CIO_AddCampany { + out companies(db:Map, addCampany(cid:Str, add:Str)) = insert(db, cid, {"add": add}) +} + +channel CIO_SetCustomerOff(uid:Str) { + out customers.{uid}.off(cid:Str, setOff(cid2)) = cid2 +} + +channel CIO_SetCompanyAdd(cid:Str) { + out companies.{cid}.add(a1:Str, setAdd(a2)) = a2 +} + +channel C(uid:Str) { + in customers.{uid}.off(cid, sync(cid2, add2)) = cid2 + in companies.{cid2}.add(a1, sync(cid2, add2)) = add2 + out customers.{uid}.add(a3:Str, sync(cid2, add2)) = add2 +} diff --git a/bin/models/Game.model b/bin/models/Game.model new file mode 100644 index 0000000..5c1eca3 --- /dev/null +++ b/bin/models/Game.model @@ -0,0 +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 +} + +channel CIO2 { + 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 +} + +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 +} + +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/bin/models/InventoryManagement.model b/bin/models/InventoryManagement.model new file mode 100644 index 0000000..578d56c --- /dev/null +++ b/bin/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/bin/models/JumpGame.model b/bin/models/JumpGame.model new file mode 100644 index 0000000..43b8d0c --- /dev/null +++ b/bin/models/JumpGame.model @@ -0,0 +1,71 @@ +init { + force := pair(0.0, 0.0) + time := 0.0 + movex := 0.0 + movey := 0.0 + mass := 1.0 + ground := true + acceleration := pair(0.0, 0.0) + velocity := pair(0.0, 0.0) + onground := true + position := pair(0.0, 0.0) + clear := false + gameover := false +} +channel CIO { + 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 +} +channel CIO3 { + out movey(y:Double, jump(y2:Double)) = y2 +} +channel CIO4 { + out mass(m:Double, setMass(x:Double)) = x +} +channel CIO5 { + 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)) +} +channel C2 { + ref onground(o, update3(a2, o)) + 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) +} +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) +} +channel C5 { + in velocity(v, update6(v2, g)) = v2 + ref ground(g, update6(v2, g)) + 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)) = (g2 == true && right(p2) <= 0.0) +} +channel C7 { + 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/bin/models/Kinematics.model b/bin/models/Kinematics.model new file mode 100644 index 0000000..4f4ab26 --- /dev/null +++ b/bin/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/bin/models/NemophilaAccounts.model b/bin/models/NemophilaAccounts.model new file mode 100644 index 0000000..c2cc23a --- /dev/null +++ b/bin/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(ontains(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/bin/models/OnlineBattleGame.model b/bin/models/OnlineBattleGame.model new file mode 100644 index 0000000..846ffbf --- /dev/null +++ b/bin/models/OnlineBattleGame.model @@ -0,0 +1,31 @@ +channel CIO_Signup{ + out accounts(adb:Map, signUp(aid:Str, name:Str)) = insert(adb, aid, {"name": name}) +} + +channel CIO_ChangeName(aid:Str) { + out accounts.{aid}.name(prev_name:Str, changeName(name)) = name +} + +channel CIO_CreateRoom { + out rooms(rdb:Map, createRoom(rid:Str, blue_id:Str, red_id:Str)) = insert(rdb, rid, {"blue_id": blue_id, "red_id": red_id}) +} + +channel CIO_ChangeRed_id(rid:Str) { + out rooms.{rid}.red_id(prev_red_id:Str, changeRed_id(red_id)) = red_id +} + +channel CIO_ChangeBlue_id(rid:Str) { + out rooms.{rid}.blue_id(prev_blue_id:Str, changeBlue_id(blue_id)) = blue_id +} + +channel C_red(rid:Str) { + in rooms.{rid}.red_id(prev_aid:Str, sync(aid, name)) = aid + in accounts.{aid}.name(prev_name:Str, sync(aid, name)) = name + out rooms.{rid}.red_name(prev_name:Str, sync(aid, name)) = name +} + +channel C_blue(rid:Str) { + in rooms.{rid}.blue_id(prev_aid:Str, sync(aid, name)) = aid + in accounts.{aid}.name(prev_name:Str, sync(aid, name)) = name + out rooms.{rid}.blue_name(prev_name:Str, sync(aid, name)) = name +} \ No newline at end of file diff --git a/bin/models/POS.dtram b/bin/models/POS.dtram new file mode 100644 index 0000000..d1cb11c --- /dev/null +++ b/bin/models/POS.dtram @@ -0,0 +1,27 @@ +model { +channel CIO { + out payment(p:Int, purchase(x:Int)) = x +} +channel C3 { + 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) +} +channel C2 { + in payment(p, update2(z)) = z + out history(h:List, update2(z)) = cons(z, h) +} +} +geometry { + node c C3:850,90,30,30 + node c C1:500,20,30,30 + node c C2:500,90,30,30 + node r total:1000,90,80,30 + node r payment:300,55,80,30 + node r history:650,90,80,30 + node r points:650,20,80,30 + node ioc CIO:150,55,30,30 +} \ No newline at end of file diff --git a/bin/models/POS.model b/bin/models/POS.model new file mode 100644 index 0000000..c15c931 --- /dev/null +++ b/bin/models/POS.model @@ -0,0 +1,15 @@ +channel CIO { + out payment(p:Int, purchase(x:Int)) = x +} +channel C3 { + 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) +} +channel C2 { + in payment(p, update2(z)) = z + out history(h:List, update2(z)) = cons(z, h) +} diff --git a/bin/models/POS2.model b/bin/models/POS2.model new file mode 100644 index 0000000..2a4196b --- /dev/null +++ b/bin/models/POS2.model @@ -0,0 +1,14 @@ +channel CIO { + 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) +} + +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 +} \ No newline at end of file diff --git a/bin/models/SimpleAddressBook.model b/bin/models/SimpleAddressBook.model new file mode 100644 index 0000000..9a9f38a --- /dev/null +++ b/bin/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/bin/models/SimpleTwitter.model b/bin/models/SimpleTwitter.model new file mode 100644 index 0000000..486fafb --- /dev/null +++ b/bin/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/bin/models/SimpleUI.model b/bin/models/SimpleUI.model new file mode 100644 index 0000000..584d8e3 --- /dev/null +++ b/bin/models/SimpleUI.model @@ -0,0 +1,31 @@ +native channel ScreenUpdate { + in screen(curSc: Json, update(nextSc)) = nextSc +} + +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 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 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 AddInputText { + out screen.widgets(widgets: Map, addInputText(wid: Str)) = insert(widgets, wid, {"type": "inputText", "state": 0}) +} diff --git a/bin/models/StockManagement.model b/bin/models/StockManagement.model new file mode 100644 index 0000000..e504d34 --- /dev/null +++ b/bin/models/StockManagement.model @@ -0,0 +1,50 @@ +init { + stock := nil + shortage := nil +} + +channel CIO_enter { + 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) +} + +channel C1 { + 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))) +} + +channel C2 { + in available(av, update2(av2, sh)) = av2 + ref shortage(sh, update2(av2, sh)) + 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(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))) +} + +channel C4 { + 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 + ref stock(st, update5(rq2, st)) + 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(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/bin/models/StockManagement2.model b/bin/models/StockManagement2.model new file mode 100644 index 0000000..857b581 --- /dev/null +++ b/bin/models/StockManagement2.model @@ -0,0 +1,13 @@ +init { + stock := nil + shortage := nil +} + +channel CIO_enter { + out deriver(s:Tuple, arrive(item:Str, num:Int)) = tuple(item, num, num) +} + +channel C3 { + in deriver(dr, update3(dr2)) = dr2 + out shipping(sp:Tuple, update3(dr2)) = tuple(fst(dr2), fst(snd(dr2))) +} diff --git a/bin/models/TravelDistance.model b/bin/models/TravelDistance.model new file mode 100644 index 0000000..07d12db --- /dev/null +++ b/bin/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/bin/models/Triangle.model b/bin/models/Triangle.model new file mode 100644 index 0000000..cf3d0e0 --- /dev/null +++ b/bin/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/bin/models/Triangle2.model b/bin/models/Triangle2.model new file mode 100644 index 0000000..5067fa0 --- /dev/null +++ b/bin/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/bin/models/Twitter.model b/bin/models/Twitter.model new file mode 100644 index 0000000..887f76f --- /dev/null +++ b/bin/models/Twitter.model @@ -0,0 +1,16 @@ +channel CIO1(myId:Str) { + out accounts(ac:List, signup(name:Str)) = cons(tuple(name, nil, nil), t1) +} + +channel CIO2(id:Str) { + out accounts.{id}.tweets(t1:List, tweet(text:Str, time:Long)) = cons(tuple(time, text), t1) +} + +channel C(myId:Str; m:Json) { + in accounts.{myId}.tweets(t1:List, m) = m.myTweets + sub C2(no:Int; flw:Json := m.followees.{no}) { + in accounts.{myId}.followees.{no}(id:Str, flw) = flw.id + in accounts.{flw.id}.tweets(t2:List, flw) = flw.tweets + } + out accounts.{myId}.timeline(l:List, m) = merge(m.myTweets, m.followees) +} \ No newline at end of file diff --git a/bin/models/WOS.dtram b/bin/models/WOS.dtram new file mode 100644 index 0000000..81b0779 --- /dev/null +++ b/bin/models/WOS.dtram @@ -0,0 +1,25 @@ +model { +channel CIO2 { + out highest(h:Double, reset(v)) = v +} +channel CIO1 { + 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 +} +channel C2{ + in temp_f(q:Double, update(y)) = y + out highest(h:Double, update(z)) = if(z >= h, z, h) +} +} +geometry { + node c C1:500,200,30,30 + node c C2:500,100,30,30 + node r highest:650,100,80,30 + node r temp_c:650,200,80,30 + node r temp_f:250,100,80,30 + node ioc CIO2:100,300,30,30 + node ioc CIO1:100,100,30,30 +} \ No newline at end of file diff --git a/bin/models/WeatherObservationSystem.model b/bin/models/WeatherObservationSystem.model new file mode 100644 index 0000000..0096407 --- /dev/null +++ b/bin/models/WeatherObservationSystem.model @@ -0,0 +1,14 @@ +channel CIO2 { + out highest(h:Double, reset(v)) = v +} +channel CIO1 { + 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 +} +channel C2{ + in temp_f(q:Double, update(y)) = y + out highest(h:Double, update(z)) = if(z >= h, z, h) +} diff --git a/bin/mvnw b/bin/mvnw new file mode 100644 index 0000000..19529dd --- /dev/null +++ b/bin/mvnw @@ -0,0 +1,259 @@ +#!/bin/sh +# ---------------------------------------------------------------------------- +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. +# ---------------------------------------------------------------------------- + +# ---------------------------------------------------------------------------- +# Apache Maven Wrapper startup batch script, version 3.3.2 +# +# Optional ENV vars +# ----------------- +# JAVA_HOME - location of a JDK home dir, required when download maven via java source +# MVNW_REPOURL - repo url base for downloading maven distribution +# MVNW_USERNAME/MVNW_PASSWORD - user and password for downloading maven +# MVNW_VERBOSE - true: enable verbose log; debug: trace the mvnw script; others: silence the output +# ---------------------------------------------------------------------------- + +set -euf +[ "${MVNW_VERBOSE-}" != debug ] || set -x + +# OS specific support. +native_path() { printf %s\\n "$1"; } +case "$(uname)" in +CYGWIN* | MINGW*) + [ -z "${JAVA_HOME-}" ] || JAVA_HOME="$(cygpath --unix "$JAVA_HOME")" + native_path() { cygpath --path --windows "$1"; } + ;; +esac + +# set JAVACMD and JAVACCMD +set_java_home() { + # For Cygwin and MinGW, ensure paths are in Unix format before anything is touched + if [ -n "${JAVA_HOME-}" ]; then + if [ -x "$JAVA_HOME/jre/sh/java" ]; then + # IBM's JDK on AIX uses strange locations for the executables + JAVACMD="$JAVA_HOME/jre/sh/java" + JAVACCMD="$JAVA_HOME/jre/sh/javac" + else + JAVACMD="$JAVA_HOME/bin/java" + JAVACCMD="$JAVA_HOME/bin/javac" + + if [ ! -x "$JAVACMD" ] || [ ! -x "$JAVACCMD" ]; then + echo "The JAVA_HOME environment variable is not defined correctly, so mvnw cannot run." >&2 + echo "JAVA_HOME is set to \"$JAVA_HOME\", but \"\$JAVA_HOME/bin/java\" or \"\$JAVA_HOME/bin/javac\" does not exist." >&2 + return 1 + fi + fi + else + JAVACMD="$( + 'set' +e + 'unset' -f command 2>/dev/null + 'command' -v java + )" || : + JAVACCMD="$( + 'set' +e + 'unset' -f command 2>/dev/null + 'command' -v javac + )" || : + + if [ ! -x "${JAVACMD-}" ] || [ ! -x "${JAVACCMD-}" ]; then + echo "The java/javac command does not exist in PATH nor is JAVA_HOME set, so mvnw cannot run." >&2 + return 1 + fi + fi +} + +# hash string like Java String::hashCode +hash_string() { + str="${1:-}" h=0 + while [ -n "$str" ]; do + char="${str%"${str#?}"}" + h=$(((h * 31 + $(LC_CTYPE=C printf %d "'$char")) % 4294967296)) + str="${str#?}" + done + printf %x\\n $h +} + +verbose() { :; } +[ "${MVNW_VERBOSE-}" != true ] || verbose() { printf %s\\n "${1-}"; } + +die() { + printf %s\\n "$1" >&2 + exit 1 +} + +trim() { + # MWRAPPER-139: + # Trims trailing and leading whitespace, carriage returns, tabs, and linefeeds. + # Needed for removing poorly interpreted newline sequences when running in more + # exotic environments such as mingw bash on Windows. + printf "%s" "${1}" | tr -d '[:space:]' +} + +# parse distributionUrl and optional distributionSha256Sum, requires .mvn/wrapper/maven-wrapper.properties +while IFS="=" read -r key value; do + case "${key-}" in + distributionUrl) distributionUrl=$(trim "${value-}") ;; + distributionSha256Sum) distributionSha256Sum=$(trim "${value-}") ;; + esac +done <"${0%/*}/.mvn/wrapper/maven-wrapper.properties" +[ -n "${distributionUrl-}" ] || die "cannot read distributionUrl property in ${0%/*}/.mvn/wrapper/maven-wrapper.properties" + +case "${distributionUrl##*/}" in +maven-mvnd-*bin.*) + MVN_CMD=mvnd.sh _MVNW_REPO_PATTERN=/maven/mvnd/ + case "${PROCESSOR_ARCHITECTURE-}${PROCESSOR_ARCHITEW6432-}:$(uname -a)" in + *AMD64:CYGWIN* | *AMD64:MINGW*) distributionPlatform=windows-amd64 ;; + :Darwin*x86_64) distributionPlatform=darwin-amd64 ;; + :Darwin*arm64) distributionPlatform=darwin-aarch64 ;; + :Linux*x86_64*) distributionPlatform=linux-amd64 ;; + *) + echo "Cannot detect native platform for mvnd on $(uname)-$(uname -m), use pure java version" >&2 + distributionPlatform=linux-amd64 + ;; + esac + distributionUrl="${distributionUrl%-bin.*}-$distributionPlatform.zip" + ;; +maven-mvnd-*) MVN_CMD=mvnd.sh _MVNW_REPO_PATTERN=/maven/mvnd/ ;; +*) MVN_CMD="mvn${0##*/mvnw}" _MVNW_REPO_PATTERN=/org/apache/maven/ ;; +esac + +# apply MVNW_REPOURL and calculate MAVEN_HOME +# maven home pattern: ~/.m2/wrapper/dists/{apache-maven-,maven-mvnd--}/ +[ -z "${MVNW_REPOURL-}" ] || distributionUrl="$MVNW_REPOURL$_MVNW_REPO_PATTERN${distributionUrl#*"$_MVNW_REPO_PATTERN"}" +distributionUrlName="${distributionUrl##*/}" +distributionUrlNameMain="${distributionUrlName%.*}" +distributionUrlNameMain="${distributionUrlNameMain%-bin}" +MAVEN_USER_HOME="${MAVEN_USER_HOME:-${HOME}/.m2}" +MAVEN_HOME="${MAVEN_USER_HOME}/wrapper/dists/${distributionUrlNameMain-}/$(hash_string "$distributionUrl")" + +exec_maven() { + unset MVNW_VERBOSE MVNW_USERNAME MVNW_PASSWORD MVNW_REPOURL || : + exec "$MAVEN_HOME/bin/$MVN_CMD" "$@" || die "cannot exec $MAVEN_HOME/bin/$MVN_CMD" +} + +if [ -d "$MAVEN_HOME" ]; then + verbose "found existing MAVEN_HOME at $MAVEN_HOME" + exec_maven "$@" +fi + +case "${distributionUrl-}" in +*?-bin.zip | *?maven-mvnd-?*-?*.zip) ;; +*) die "distributionUrl is not valid, must match *-bin.zip or maven-mvnd-*.zip, but found '${distributionUrl-}'" ;; +esac + +# prepare tmp dir +if TMP_DOWNLOAD_DIR="$(mktemp -d)" && [ -d "$TMP_DOWNLOAD_DIR" ]; then + clean() { rm -rf -- "$TMP_DOWNLOAD_DIR"; } + trap clean HUP INT TERM EXIT +else + die "cannot create temp dir" +fi + +mkdir -p -- "${MAVEN_HOME%/*}" + +# Download and Install Apache Maven +verbose "Couldn't find MAVEN_HOME, downloading and installing it ..." +verbose "Downloading from: $distributionUrl" +verbose "Downloading to: $TMP_DOWNLOAD_DIR/$distributionUrlName" + +# select .zip or .tar.gz +if ! command -v unzip >/dev/null; then + distributionUrl="${distributionUrl%.zip}.tar.gz" + distributionUrlName="${distributionUrl##*/}" +fi + +# verbose opt +__MVNW_QUIET_WGET=--quiet __MVNW_QUIET_CURL=--silent __MVNW_QUIET_UNZIP=-q __MVNW_QUIET_TAR='' +[ "${MVNW_VERBOSE-}" != true ] || __MVNW_QUIET_WGET='' __MVNW_QUIET_CURL='' __MVNW_QUIET_UNZIP='' __MVNW_QUIET_TAR=v + +# normalize http auth +case "${MVNW_PASSWORD:+has-password}" in +'') MVNW_USERNAME='' MVNW_PASSWORD='' ;; +has-password) [ -n "${MVNW_USERNAME-}" ] || MVNW_USERNAME='' MVNW_PASSWORD='' ;; +esac + +if [ -z "${MVNW_USERNAME-}" ] && command -v wget >/dev/null; then + verbose "Found wget ... using wget" + wget ${__MVNW_QUIET_WGET:+"$__MVNW_QUIET_WGET"} "$distributionUrl" -O "$TMP_DOWNLOAD_DIR/$distributionUrlName" || die "wget: Failed to fetch $distributionUrl" +elif [ -z "${MVNW_USERNAME-}" ] && command -v curl >/dev/null; then + verbose "Found curl ... using curl" + curl ${__MVNW_QUIET_CURL:+"$__MVNW_QUIET_CURL"} -f -L -o "$TMP_DOWNLOAD_DIR/$distributionUrlName" "$distributionUrl" || die "curl: Failed to fetch $distributionUrl" +elif set_java_home; then + verbose "Falling back to use Java to download" + javaSource="$TMP_DOWNLOAD_DIR/Downloader.java" + targetZip="$TMP_DOWNLOAD_DIR/$distributionUrlName" + cat >"$javaSource" <<-END + public class Downloader extends java.net.Authenticator + { + protected java.net.PasswordAuthentication getPasswordAuthentication() + { + return new java.net.PasswordAuthentication( System.getenv( "MVNW_USERNAME" ), System.getenv( "MVNW_PASSWORD" ).toCharArray() ); + } + public static void main( String[] args ) throws Exception + { + setDefault( new Downloader() ); + java.nio.file.Files.copy( java.net.URI.create( args[0] ).toURL().openStream(), java.nio.file.Paths.get( args[1] ).toAbsolutePath().normalize() ); + } + } + END + # For Cygwin/MinGW, switch paths to Windows format before running javac and java + verbose " - Compiling Downloader.java ..." + "$(native_path "$JAVACCMD")" "$(native_path "$javaSource")" || die "Failed to compile Downloader.java" + verbose " - Running Downloader.java ..." + "$(native_path "$JAVACMD")" -cp "$(native_path "$TMP_DOWNLOAD_DIR")" Downloader "$distributionUrl" "$(native_path "$targetZip")" +fi + +# If specified, validate the SHA-256 sum of the Maven distribution zip file +if [ -n "${distributionSha256Sum-}" ]; then + distributionSha256Result=false + if [ "$MVN_CMD" = mvnd.sh ]; then + echo "Checksum validation is not supported for maven-mvnd." >&2 + echo "Please disable validation by removing 'distributionSha256Sum' from your maven-wrapper.properties." >&2 + exit 1 + elif command -v sha256sum >/dev/null; then + if echo "$distributionSha256Sum $TMP_DOWNLOAD_DIR/$distributionUrlName" | sha256sum -c >/dev/null 2>&1; then + distributionSha256Result=true + fi + elif command -v shasum >/dev/null; then + if echo "$distributionSha256Sum $TMP_DOWNLOAD_DIR/$distributionUrlName" | shasum -a 256 -c >/dev/null 2>&1; then + distributionSha256Result=true + fi + else + echo "Checksum validation was requested but neither 'sha256sum' or 'shasum' are available." >&2 + echo "Please install either command, or disable validation by removing 'distributionSha256Sum' from your maven-wrapper.properties." >&2 + exit 1 + fi + if [ $distributionSha256Result = false ]; then + echo "Error: Failed to validate Maven distribution SHA-256, your Maven distribution might be compromised." >&2 + echo "If you updated your Maven version, you need to update the specified distributionSha256Sum property." >&2 + exit 1 + fi +fi + +# unzip and move +if command -v unzip >/dev/null; then + unzip ${__MVNW_QUIET_UNZIP:+"$__MVNW_QUIET_UNZIP"} "$TMP_DOWNLOAD_DIR/$distributionUrlName" -d "$TMP_DOWNLOAD_DIR" || die "failed to unzip" +else + tar xzf${__MVNW_QUIET_TAR:+"$__MVNW_QUIET_TAR"} "$TMP_DOWNLOAD_DIR/$distributionUrlName" -C "$TMP_DOWNLOAD_DIR" || die "failed to untar" +fi +printf %s\\n "$distributionUrl" >"$TMP_DOWNLOAD_DIR/$distributionUrlNameMain/mvnw.url" +mv -- "$TMP_DOWNLOAD_DIR/$distributionUrlNameMain" "$MAVEN_HOME" || [ -d "$MAVEN_HOME" ] || die "fail to move MAVEN_HOME" + +clean || : +exec_maven "$@" diff --git a/bin/mvnw.cmd b/bin/mvnw.cmd new file mode 100644 index 0000000..249bdf3 --- /dev/null +++ b/bin/mvnw.cmd @@ -0,0 +1,149 @@ +<# : batch portion +@REM ---------------------------------------------------------------------------- +@REM Licensed to the Apache Software Foundation (ASF) under one +@REM or more contributor license agreements. See the NOTICE file +@REM distributed with this work for additional information +@REM regarding copyright ownership. The ASF licenses this file +@REM to you under the Apache License, Version 2.0 (the +@REM "License"); you may not use this file except in compliance +@REM with the License. You may obtain a copy of the License at +@REM +@REM http://www.apache.org/licenses/LICENSE-2.0 +@REM +@REM Unless required by applicable law or agreed to in writing, +@REM software distributed under the License is distributed on an +@REM "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +@REM KIND, either express or implied. See the License for the +@REM specific language governing permissions and limitations +@REM under the License. +@REM ---------------------------------------------------------------------------- + +@REM ---------------------------------------------------------------------------- +@REM Apache Maven Wrapper startup batch script, version 3.3.2 +@REM +@REM Optional ENV vars +@REM MVNW_REPOURL - repo url base for downloading maven distribution +@REM MVNW_USERNAME/MVNW_PASSWORD - user and password for downloading maven +@REM MVNW_VERBOSE - true: enable verbose log; others: silence the output +@REM ---------------------------------------------------------------------------- + +@IF "%__MVNW_ARG0_NAME__%"=="" (SET __MVNW_ARG0_NAME__=%~nx0) +@SET __MVNW_CMD__= +@SET __MVNW_ERROR__= +@SET __MVNW_PSMODULEP_SAVE=%PSModulePath% +@SET PSModulePath= +@FOR /F "usebackq tokens=1* delims==" %%A IN (`powershell -noprofile "& {$scriptDir='%~dp0'; $script='%__MVNW_ARG0_NAME__%'; icm -ScriptBlock ([Scriptblock]::Create((Get-Content -Raw '%~f0'))) -NoNewScope}"`) DO @( + IF "%%A"=="MVN_CMD" (set __MVNW_CMD__=%%B) ELSE IF "%%B"=="" (echo %%A) ELSE (echo %%A=%%B) +) +@SET PSModulePath=%__MVNW_PSMODULEP_SAVE% +@SET __MVNW_PSMODULEP_SAVE= +@SET __MVNW_ARG0_NAME__= +@SET MVNW_USERNAME= +@SET MVNW_PASSWORD= +@IF NOT "%__MVNW_CMD__%"=="" (%__MVNW_CMD__% %*) +@echo Cannot start maven from wrapper >&2 && exit /b 1 +@GOTO :EOF +: end batch / begin powershell #> + +$ErrorActionPreference = "Stop" +if ($env:MVNW_VERBOSE -eq "true") { + $VerbosePreference = "Continue" +} + +# calculate distributionUrl, requires .mvn/wrapper/maven-wrapper.properties +$distributionUrl = (Get-Content -Raw "$scriptDir/.mvn/wrapper/maven-wrapper.properties" | ConvertFrom-StringData).distributionUrl +if (!$distributionUrl) { + Write-Error "cannot read distributionUrl property in $scriptDir/.mvn/wrapper/maven-wrapper.properties" +} + +switch -wildcard -casesensitive ( $($distributionUrl -replace '^.*/','') ) { + "maven-mvnd-*" { + $USE_MVND = $true + $distributionUrl = $distributionUrl -replace '-bin\.[^.]*$',"-windows-amd64.zip" + $MVN_CMD = "mvnd.cmd" + break + } + default { + $USE_MVND = $false + $MVN_CMD = $script -replace '^mvnw','mvn' + break + } +} + +# apply MVNW_REPOURL and calculate MAVEN_HOME +# maven home pattern: ~/.m2/wrapper/dists/{apache-maven-,maven-mvnd--}/ +if ($env:MVNW_REPOURL) { + $MVNW_REPO_PATTERN = if ($USE_MVND) { "/org/apache/maven/" } else { "/maven/mvnd/" } + $distributionUrl = "$env:MVNW_REPOURL$MVNW_REPO_PATTERN$($distributionUrl -replace '^.*'+$MVNW_REPO_PATTERN,'')" +} +$distributionUrlName = $distributionUrl -replace '^.*/','' +$distributionUrlNameMain = $distributionUrlName -replace '\.[^.]*$','' -replace '-bin$','' +$MAVEN_HOME_PARENT = "$HOME/.m2/wrapper/dists/$distributionUrlNameMain" +if ($env:MAVEN_USER_HOME) { + $MAVEN_HOME_PARENT = "$env:MAVEN_USER_HOME/wrapper/dists/$distributionUrlNameMain" +} +$MAVEN_HOME_NAME = ([System.Security.Cryptography.MD5]::Create().ComputeHash([byte[]][char[]]$distributionUrl) | ForEach-Object {$_.ToString("x2")}) -join '' +$MAVEN_HOME = "$MAVEN_HOME_PARENT/$MAVEN_HOME_NAME" + +if (Test-Path -Path "$MAVEN_HOME" -PathType Container) { + Write-Verbose "found existing MAVEN_HOME at $MAVEN_HOME" + Write-Output "MVN_CMD=$MAVEN_HOME/bin/$MVN_CMD" + exit $? +} + +if (! $distributionUrlNameMain -or ($distributionUrlName -eq $distributionUrlNameMain)) { + Write-Error "distributionUrl is not valid, must end with *-bin.zip, but found $distributionUrl" +} + +# prepare tmp dir +$TMP_DOWNLOAD_DIR_HOLDER = New-TemporaryFile +$TMP_DOWNLOAD_DIR = New-Item -Itemtype Directory -Path "$TMP_DOWNLOAD_DIR_HOLDER.dir" +$TMP_DOWNLOAD_DIR_HOLDER.Delete() | Out-Null +trap { + if ($TMP_DOWNLOAD_DIR.Exists) { + try { Remove-Item $TMP_DOWNLOAD_DIR -Recurse -Force | Out-Null } + catch { Write-Warning "Cannot remove $TMP_DOWNLOAD_DIR" } + } +} + +New-Item -Itemtype Directory -Path "$MAVEN_HOME_PARENT" -Force | Out-Null + +# Download and Install Apache Maven +Write-Verbose "Couldn't find MAVEN_HOME, downloading and installing it ..." +Write-Verbose "Downloading from: $distributionUrl" +Write-Verbose "Downloading to: $TMP_DOWNLOAD_DIR/$distributionUrlName" + +$webclient = New-Object System.Net.WebClient +if ($env:MVNW_USERNAME -and $env:MVNW_PASSWORD) { + $webclient.Credentials = New-Object System.Net.NetworkCredential($env:MVNW_USERNAME, $env:MVNW_PASSWORD) +} +[Net.ServicePointManager]::SecurityProtocol = [Net.SecurityProtocolType]::Tls12 +$webclient.DownloadFile($distributionUrl, "$TMP_DOWNLOAD_DIR/$distributionUrlName") | Out-Null + +# If specified, validate the SHA-256 sum of the Maven distribution zip file +$distributionSha256Sum = (Get-Content -Raw "$scriptDir/.mvn/wrapper/maven-wrapper.properties" | ConvertFrom-StringData).distributionSha256Sum +if ($distributionSha256Sum) { + if ($USE_MVND) { + Write-Error "Checksum validation is not supported for maven-mvnd. `nPlease disable validation by removing 'distributionSha256Sum' from your maven-wrapper.properties." + } + Import-Module $PSHOME\Modules\Microsoft.PowerShell.Utility -Function Get-FileHash + if ((Get-FileHash "$TMP_DOWNLOAD_DIR/$distributionUrlName" -Algorithm SHA256).Hash.ToLower() -ne $distributionSha256Sum) { + Write-Error "Error: Failed to validate Maven distribution SHA-256, your Maven distribution might be compromised. If you updated your Maven version, you need to update the specified distributionSha256Sum property." + } +} + +# unzip and move +Expand-Archive "$TMP_DOWNLOAD_DIR/$distributionUrlName" -DestinationPath "$TMP_DOWNLOAD_DIR" | Out-Null +Rename-Item -Path "$TMP_DOWNLOAD_DIR/$distributionUrlNameMain" -NewName $MAVEN_HOME_NAME | Out-Null +try { + Move-Item -Path "$TMP_DOWNLOAD_DIR/$MAVEN_HOME_NAME" -Destination $MAVEN_HOME_PARENT | Out-Null +} catch { + if (! (Test-Path -Path "$MAVEN_HOME" -PathType Container)) { + Write-Error "fail to move MAVEN_HOME" + } +} finally { + try { Remove-Item $TMP_DOWNLOAD_DIR -Recurse -Force | Out-Null } + catch { Write-Warning "Cannot remove $TMP_DOWNLOAD_DIR" } +} + +Write-Output "MVN_CMD=$MAVEN_HOME/bin/$MVN_CMD" diff --git a/bin/pom.xml b/bin/pom.xml new file mode 100644 index 0000000..991d5f1 --- /dev/null +++ b/bin/pom.xml @@ -0,0 +1,94 @@ + + + 4.0.0 + + org.springframework.boot + spring-boot-starter-parent + 3.3.3 + + + com.example + DTRAMServer + 0.0.1-SNAPSHOT + DTRAMServer + Demo project for Spring Boot + + + + + + + + + + + + + + + 17 + + + + org.springframework.boot + spring-boot-starter-data-jdbc + + + org.springframework.boot + spring-boot-starter-data-jpa + + + org.springframework.boot + spring-boot-starter-thymeleaf + + + org.springframework.boot + spring-boot-starter-web + + + + org.springframework.boot + spring-boot-devtools + runtime + true + + + com.h2database + h2 + runtime + + + org.projectlombok + lombok + true + + + org.springframework.boot + spring-boot-starter-test + test + + + org.springframework.boot + spring-boot-starter-websocket + + + + + + + org.springframework.boot + spring-boot-maven-plugin + + + + org.projectlombok + lombok + + + + + + + + diff --git a/bin/src/main/java/com/example/test/DtramServerApplication.class b/bin/src/main/java/com/example/test/DtramServerApplication.class new file mode 100644 index 0000000..346ded8 --- /dev/null +++ b/bin/src/main/java/com/example/test/DtramServerApplication.class Binary files differ diff --git a/bin/src/main/java/com/example/test/controller/SimulatPageController.class b/bin/src/main/java/com/example/test/controller/SimulatPageController.class new file mode 100644 index 0000000..89c2d1c --- /dev/null +++ b/bin/src/main/java/com/example/test/controller/SimulatPageController.class Binary files differ diff --git a/bin/src/main/java/com/example/test/dtram/Dtram.class b/bin/src/main/java/com/example/test/dtram/Dtram.class new file mode 100644 index 0000000..d23e92e --- /dev/null +++ b/bin/src/main/java/com/example/test/dtram/Dtram.class Binary files differ diff --git a/bin/src/main/java/com/example/test/rest_controllers/OpenModelController.class b/bin/src/main/java/com/example/test/rest_controllers/OpenModelController.class new file mode 100644 index 0000000..666e106 --- /dev/null +++ b/bin/src/main/java/com/example/test/rest_controllers/OpenModelController.class Binary files differ diff --git a/bin/src/main/java/com/example/test/services/ModelHandleService.class b/bin/src/main/java/com/example/test/services/ModelHandleService.class new file mode 100644 index 0000000..b699a3a --- /dev/null +++ b/bin/src/main/java/com/example/test/services/ModelHandleService.class Binary files differ diff --git a/bin/src/main/java/com/example/test/websocket/WebSocketConfig.class b/bin/src/main/java/com/example/test/websocket/WebSocketConfig.class new file mode 100644 index 0000000..7035658 --- /dev/null +++ b/bin/src/main/java/com/example/test/websocket/WebSocketConfig.class Binary files differ diff --git a/bin/src/main/java/com/example/test/websocket/WebSocketHandler.class b/bin/src/main/java/com/example/test/websocket/WebSocketHandler.class new file mode 100644 index 0000000..e73e8e2 --- /dev/null +++ b/bin/src/main/java/com/example/test/websocket/WebSocketHandler.class Binary files differ diff --git a/bin/src/main/resources/application.properties b/bin/src/main/resources/application.properties new file mode 100644 index 0000000..ec8b7f3 --- /dev/null +++ b/bin/src/main/resources/application.properties @@ -0,0 +1 @@ +spring.application.name=DTRAMServer diff --git a/bin/src/main/resources/static/simulator_ws.js b/bin/src/main/resources/static/simulator_ws.js new file mode 100644 index 0000000..ece2a6e --- /dev/null +++ b/bin/src/main/resources/static/simulator_ws.js @@ -0,0 +1,20 @@ +let socket = new WebSocket("ws://localhost:8080/ws"); + +socket.onmessage = function(event) { + + console.log(event.data); + + +} + +socket.onopen = function(event) { + console.log("open socket"); +} + +socket.onclose = function(event) { + console.log("close socket"); +} + +socket.onerror = function(event) { + console.log("error"); +} \ No newline at end of file diff --git a/bin/src/main/resources/templates/index.html b/bin/src/main/resources/templates/index.html new file mode 100644 index 0000000..2571001 --- /dev/null +++ b/bin/src/main/resources/templates/index.html @@ -0,0 +1,10 @@ + + + + +Insert title here + + + + + \ No newline at end of file diff --git a/bin/src/main/resources/templates/simulator.html b/bin/src/main/resources/templates/simulator.html new file mode 100644 index 0000000..4f2516b --- /dev/null +++ b/bin/src/main/resources/templates/simulator.html @@ -0,0 +1,11 @@ + + + + +Insert title here + + +
+ + + \ No newline at end of file diff --git a/bin/src/test/java/com/example/test/DtramServerApplicationTests.class b/bin/src/test/java/com/example/test/DtramServerApplicationTests.class new file mode 100644 index 0000000..6e4109c --- /dev/null +++ b/bin/src/test/java/com/example/test/DtramServerApplicationTests.class Binary files differ diff --git a/models/SimpleUI2.model b/models/SimpleUI2.model index 9af9a97..eb10c6a 100644 --- a/models/SimpleUI2.model +++ b/models/SimpleUI2.model @@ -1,40 +1,10 @@ init { - screen := { - "widgets": { - "001": { - "type": "button", - "text": "a", - "state": 0, - "x": 100, - "y": 100, - "width": 100, - "height": 40, - "onPressed": { - "method": "a" - } - }, - "002": {"type": "textInput", "text": "", "state": 0}, - "003": { - "type": "button", - "text": "change", - "state": 0, - "x": 50, - "y": 50, - "width": 100, - "height": 40, - "onPressed": { - "method": "transition", - "data": { - "widgets": { - "004": {"type": "label", "text": "hello", "state": 0, "x": 100, "y": 100} - }, - "layout": true - } - } - } - }, - "layout": true - } + variables := { + "a": { + "from": "001", + "to": "002" + } + } } native channel ScreenUpdate { @@ -69,7 +39,9 @@ out screen.widgets(widgets: Map, addTextInput(wid: Str)) = insert(widgets, wid, {"type": "textInput", "text": "", "state": 0}) } -channel Test(wid: Str) { - in screen.widgets.{wid}.state(curState: Int, test(nextState: Str, wid: Str)) = nextState - out screen.widgets.{wid}.text(curText: Str, test(nextState: Str, wid: Str)) = if(wid == "001", "hello", curText) +channel ChangeText(wid: Str) { + ref variables.a.from(from, updateText(from, to, newText)) + ref variables.a.to(to, updateText(from, to, nexText)) + in screen.widgets.{wid}.text(curText: Str, updateText(from, to, nexText)) = curText + out screen.widgets.{to}.text(curText: Str, updateText(from, to, nexText)) = if(wid == from, nextText, curText) } diff --git a/src/main/java/com/example/test/dtram/Dtram.java b/src/main/java/com/example/test/dtram/Dtram.java index 270fffd..5bdb70f 100644 --- a/src/main/java/com/example/test/dtram/Dtram.java +++ b/src/main/java/com/example/test/dtram/Dtram.java @@ -2,48 +2,65 @@ import java.io.BufferedReader; import java.io.File; -import java.io.FileReader; import java.io.InputStream; import java.io.InputStreamReader; +import java.io.StringReader; import java.nio.charset.StandardCharsets; -import java.util.HashMap; -import java.util.Map; import org.springframework.stereotype.Component; +import com.example.test.websocket.WebSocketHandler; + +import java.util.HashMap; +import java.util.Map; + +import algorithms.TypeInference; import models.dataConstraintModel.JsonTerm; import models.dataFlowModel.DataTransferModel; import parser.Parser; import simulator.Simulator; import simulator.interfaces.html.HtmlElement; import simulator.interfaces.html.HtmlPresenter; -import simulator.interfaces.html.IWebSocketMessageSender; @Component -public class Dtram { +public class Dtram{ File file; DataTransferModel model; Simulator simulator; - private final IWebSocketMessageSender ws; + private final WebSocketHandler ws; private Map elements; HtmlPresenter presenter; - Dtram(IWebSocketMessageSender ws){ + Dtram(WebSocketHandler ws){ this.ws = ws; elements = new HashMap<>(); } - public void initModel(String path) { - file = new File(path); - System.out.println(path); +// public void initModel(String path) { +// file = new File(path); +// System.out.println(path); +// try { +// Parser parser = new Parser(new BufferedReader(new FileReader(file))); +// model = parser.doParse(); +// }catch(Exception e) { +// e.printStackTrace(); +// } +// } + + public void initModel(String modelText) { + + StringReader stringReader = new StringReader(modelText); + BufferedReader bufferedReader = new BufferedReader(stringReader); try { - Parser parser = new Parser(new BufferedReader(new FileReader(file))); + Parser parser = new Parser(bufferedReader); model = parser.doParse(); - }catch(Exception e) { + TypeInference.infer(model); + } + catch(Exception e) { e.printStackTrace(); } } @@ -58,17 +75,18 @@ } } - public void startSimulator() { + public void startSimulator(String sessionId) { simulator = new Simulator(model); simulator.init(); - presenter = new HtmlPresenter(simulator, ws, elements); + presenter = new HtmlPresenter(simulator, ws, elements, sessionId); } public void onRestEvent(String id, String method, JsonTerm message) { - elements.get("\"" + id + "\"").onRestEvent(method, message); + elements.get(id).onRestEvent(method, message); } - - - + public DataTransferModel getModel() { + return model; + } + } diff --git a/src/main/java/com/example/test/rest_controllers/OpenModelController.java b/src/main/java/com/example/test/rest_controllers/OpenModelController.java index ad4f985..01a21a6 100644 --- a/src/main/java/com/example/test/rest_controllers/OpenModelController.java +++ b/src/main/java/com/example/test/rest_controllers/OpenModelController.java @@ -21,15 +21,21 @@ } @PostMapping("/open_model") - public void openModel(@RequestParam("file") MultipartFile file) { + public void openModel(@RequestParam("file") MultipartFile file, @RequestParam("session_id") String sessionId) { try { - modelService.openModel(file.getInputStream()); + modelService.openModel(file.getInputStream(), sessionId); } catch (IOException e) { // TODO 自動生成された catch ブロック e.printStackTrace(); } } + @PostMapping("/open_model_text") + public void openModel(@RequestParam("model_text") String modelText, @RequestParam("session_id") String sessionId) { + System.out.println(modelText); + modelService.openModel(modelText, sessionId); + } + diff --git a/src/main/java/com/example/test/services/ElementEventService.java b/src/main/java/com/example/test/services/ElementEventService.java index 5750d9f..df41597 100644 --- a/src/main/java/com/example/test/services/ElementEventService.java +++ b/src/main/java/com/example/test/services/ElementEventService.java @@ -1,19 +1,65 @@ package com.example.test.services; import org.springframework.stereotype.Service; +import org.springframework.web.socket.WebSocketSession; import com.example.test.dtram.Dtram; +import com.example.test.websocket.IMessageReceiveListener; +import com.example.test.websocket.WebSocketHandler; import models.algebra.Constant; import models.dataConstraintModel.JsonTerm; +import parser.Parser; +import parser.Parser.TokenStream; +import parser.exceptions.ExpectedColon; +import parser.exceptions.ExpectedDoubleQuotation; +import parser.exceptions.ExpectedRightBracket; +import parser.exceptions.WrongJsonExpression; @Service -public class ElementEventService { +public class ElementEventService implements IMessageReceiveListener{ private final Dtram dtram; + private final WebSocketHandler ws; + private TokenStream stream; + private Parser parser; - ElementEventService(Dtram dtram) { + ElementEventService(Dtram dtram, WebSocketHandler ws) { this.dtram = dtram; + this.ws = ws; + this.ws.addMessageListener(this); + stream = new Parser.TokenStream(); + parser = new Parser(stream); + } + + public JsonTerm handleMessage(String message){ + stream.addLine(message); + System.out.println(message); + try { + return (JsonTerm) parser.parseTerm(stream, dtram.getModel()); + } catch (ExpectedRightBracket | WrongJsonExpression | ExpectedColon | ExpectedDoubleQuotation e) { + e.printStackTrace(); + return null; + } + } + + @Override + public void onReceivedMessage(String message, WebSocketSession session) { + JsonTerm data = handleMessage(message); + String method = (String)((Constant) data.get("method")).getValue(); + String id = (String)((Constant) data.get("id")).getValue(); + if(method.equals("connect")) { + ws.connectIdToSession(id, session); + } else if(method.equals("mouseEvent")) { + String state = (String)((Constant) data.get("state")).getValue(); + switch(state) { + case "1": onButtonPressed(id);break; + case "0": onButtonReleased(id);break; + } + } else if(method.equals("textEvent")) { + String newText = (String)((Constant) data.get("newText")).getValue(); + onTextChanged(id, newText); + } } public void onButtonPressed(String id) { @@ -29,5 +75,4 @@ json.addMember("newText", new Constant(newText)); dtram.onRestEvent(id, "onTextChanged", json); } - } diff --git a/src/main/java/com/example/test/services/ModelHandleService.java b/src/main/java/com/example/test/services/ModelHandleService.java index ae976d5..15de8e7 100644 --- a/src/main/java/com/example/test/services/ModelHandleService.java +++ b/src/main/java/com/example/test/services/ModelHandleService.java @@ -15,14 +15,14 @@ dtram = d; } - public void openModel(String path) { - dtram.initModel(path); - dtram.startSimulator(); + public void openModel(String modelText, String sessionId) { + dtram.initModel(modelText); + dtram.startSimulator(sessionId); } - public void openModel(InputStream stream) { + public void openModel(InputStream stream, String sessionId) { dtram.initModel(stream); - dtram.startSimulator(); + dtram.startSimulator(sessionId); } } diff --git a/src/main/java/com/example/test/websocket/IMessageReceiveListener.java b/src/main/java/com/example/test/websocket/IMessageReceiveListener.java new file mode 100644 index 0000000..2c7bd8d --- /dev/null +++ b/src/main/java/com/example/test/websocket/IMessageReceiveListener.java @@ -0,0 +1,9 @@ +package com.example.test.websocket; + +import org.springframework.web.socket.WebSocketSession; + +public interface IMessageReceiveListener { + + public void onReceivedMessage(String message, WebSocketSession session); + +} diff --git a/src/main/java/com/example/test/websocket/WebSocketHandler.java b/src/main/java/com/example/test/websocket/WebSocketHandler.java index 10d79b8..40a3327 100644 --- a/src/main/java/com/example/test/websocket/WebSocketHandler.java +++ b/src/main/java/com/example/test/websocket/WebSocketHandler.java @@ -1,7 +1,6 @@ package com.example.test.websocket; -import java.util.HashSet; -import java.util.Set; +import java.io.IOException; import org.springframework.stereotype.Component; import org.springframework.web.socket.CloseStatus; @@ -9,38 +8,96 @@ import org.springframework.web.socket.WebSocketSession; import org.springframework.web.socket.handler.TextWebSocketHandler; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import parser.Parser; +import parser.Parser.TokenStream; import simulator.interfaces.html.IWebSocketMessageSender; @Component public class WebSocketHandler extends TextWebSocketHandler implements IWebSocketMessageSender{ - private Set sessions = new HashSet<>(); + private Map sessions = new HashMap<>(); + private Map sessionManager = new HashMap<>(); + private Map> buffer = new HashMap<>(); + private List messageListeners; + private TokenStream stream; + private Parser parser; + + + public WebSocketHandler() { + messageListeners = new ArrayList<>(); + stream = new Parser.TokenStream(); + parser = new Parser(stream); + } + + public void addMessageListener(IMessageReceiveListener listener) { + messageListeners.add(listener); + } @Override public void afterConnectionEstablished(WebSocketSession session) throws Exception { - sessions.add(session); + System.out.println("add new session " + session.getId()); + sessions.put(session, null); } @Override public void afterConnectionClosed(WebSocketSession session, CloseStatus status) throws Exception { + System.out.println("colse session " + session.getId()); + String sessionId = sessions.get(session); sessions.remove(session); + sessionManager.remove(sessionId); } + @Override + public void handleTextMessage(WebSocketSession session, TextMessage message) throws Exception { + for(var listener : messageListeners) { + listener.onReceivedMessage(message.getPayload(), session); + } + } + public void sendMessageToAll(String message) throws Exception { - for(var session : sessions) { + for(var session : sessions.keySet()) { if(session.isOpen()) { session.sendMessage(new TextMessage(message)); } } } - + + public void connectIdToSession(String id, WebSocketSession session) { + System.out.println("receive " + id); + sessions.put(session, id); + sessionManager.put(id, session); + if(!buffer.containsKey(id)) { + return; + } + for(String mes: buffer.get(id)) { + try { + session.sendMessage(new TextMessage(mes)); + } catch (IOException e) { + e.printStackTrace(); + } + } + buffer.remove(id); + } + @Override - public void send(String message) { + public void send(String message, String sessionId) { + System.out.println("send " + message + "to " + sessionId); try { - sendMessageToAll(message); + if(sessionManager.containsKey(sessionId)) { + sessionManager.get(sessionId).sendMessage(new TextMessage(message)); + } else { + if(!buffer.containsKey(sessionId)) { + buffer.put(sessionId, new ArrayList<>()); + } + buffer.get(sessionId).add(message); + } } catch (Exception e) { - // TODO 自動生成された catch ブロック e.printStackTrace(); } }