不要なモデルの削除
1 parent efbe282 commit 99191a6b0a92c936975b323bf925ceffb962e222
Shinji authored on 20 Feb 2023
Showing 2 changed files
View
58
AlgebraicDataflowArchitectureModel/models/Algo.model 100644 → 0
init {
deck := nil
handsA := nil
handsB := nil
}
channel turnAdraw{
ref handsB(b:List, drawA(target:Int, guess:Int, b, d))
ref deck(d:List, drawA(target, guess, b, d))
out handsA(outA:List, drawA(target, guess, b, d)) == if(eq(fst(get(b, target)), guess),
sortByKey(cons(tuple(fst(head(d)),false), outA)),
sortByKey(cons(tuple(fst(head(d)), true), outA)))
out handsB(outB:List, drawA(target, guess, b, d)) == if(eq(fst(get(b, target)), guess),
set(outB, target, tuple(fst(get(outB, target)), true)),
outB)
out deck(t:List, drawA(target, guess, b, d)) == tail(d)
}
channel turnBdraw{
ref handsA(a:List, drawB(target:Int, guess:Int, a, d:List))
ref deck(d:List, drawB(target, guess, a, d))
out handsB(outB:List, drawB(target, guess, a, d)) == if(eq(fst(get(a, target)), guess),
sortByKey(cons(tuple(fst(head(d)),false), outB)),
sortByKey(cons(tuple(fst(head(d)), true), outB)))
out handsA(outA:List, drawB(target, guess, a, d)) == if(eq(fst(get(a, target)), guess),
set(outA, target, tuple(fst(get(outA, target)), true)),
outA)
out deck(t:List, drawB(target, guess, a, d)) == tail(d)
}
channel turnAselect{
ref handsB(b:List, selectA(target:Int, guess:Int, attacker:Int, b))
out handsA(outA:List, selectA(target, guess, attacker, b)) == if(eq(fst(get(b, target)), guess),
outA,
set(outA, attacker, tuple(fst(get(outA, attacker)), true)))
out handsB(outB:List, selectA(target, guess, attacker, b)) == if(eq(fst(get(b, target)), guess),
set(outB, target, tuple(fst(get(outB, target)), true)),
outB)
}
channel turnBselect{
ref handsA(a:List, selectB(target:Int, guess:Int, attacker:Int, a))
 
out handsB(outB:List, selectB(target, guess, attacker, a)) == if(eq(fst(get(a, target)), guess),
outB,
set(outB, attacker, tuple(fst(get(outB, attacker)), true)))
out handsA(outA:List, selectB(target, guess, attacker, a)) == if(eq(fst(get(a, target)), guess),
set(outA, target, tuple(fst(get(outA, target)), true)),
outA)
}
channel judgeA{
in handsA(a:List, judge(j)) == j
out loseA(la:Bool, judge(j)) == eq(length(extractFaceDown(j)), 0)
}
channel judgeB{
in handsB(b:List, judge(j)) == j
out loseB(lb:Bool, judge(j)) == eq(length(extractFaceDown(j)), 0)
}
View
14
AlgebraicDataflowArchitectureModel/models/ModTest 100644 → 0
init{
deck := nil
}
channel CIO {
out deck(s, input(x)) == x
out deck(p:List, inp(x:Tuple)) == cons(x, sortCard(cons(x, p)))
out geck(p:Int, inp(x:Tuple)) == length(sortCard(cons(x, p)))
}
channel C{
 
}