【InventoryManagement(Alloy)】

+ ここでは，InventoryManagement の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください． +

InventoryManagement の Alloy による仕様記述についての説明

sig:

+ Alloy では，商品id の集合を ItemId，商品名の集合を Name， + 商品全体を保管する倉庫の集合を Inventory，商品の集合を Item で表します．
+ 以下のモデルでは sig を用いて，ItemId，Name，Inventory，Item の順番にこれらの集合を宣言しています．
+ Inventory には，ItemId から Item への対応関係が itemDB フィールドとして定義されています．
+ ここで，ItemId の右側の lone は１つの Item に対応する ItemId がたかだか１つしかないことを示しています．
+ Item の宣言では，商品名を表す name が Name のインスタンスとして， + 在庫数を表す count が Int のインスタンスとして定義されています．
+

pred:

+ 最初の述語として記述されている init は，Inventory の + インスタンスである its が初期化されていることを示しています．
+ 次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と， + 登録した後のインスタンス its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．
+ また，述語定義中の some it: Item は，its のデータベースに登録されていない Item のインスタンス it が存在していることを示しており， + 直観的には Item のインスタンスの生成を示しています．
+ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， + 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており， + 直観的には，Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
+ 最後の execute では，init ，itemRegistraction ，receivingOrShipping を + この順で呼び出す操作を定義しています．
+ run では，execute を呼び出して仮想実行を行います． + この実行の際に，Int で8bitの整数を扱うことができるよう末尾に 8 Int という記述を付け加えています． +

+sig ItemId, Name{}
+sig Inventory {
+	itemDB: ItemId lone -> lone Item
+}
+sig Item {
+	name : Name,
+	count: Int
+}
+
+pred init[its: Inventory] {
+	no its.itemDB
+}
+
+pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
+	some it: Item | {
+		no itemId2: ItemId | its.itemDB[itemId2] = it
+		its'.itemDB = its.itemDB + itemId -> it
+		it.name = n
+		it.count = quantity
+	}
+}
+
+pred receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity: Int] {
+	some it': Item | {
+		no itemId2: ItemId | its.itemDB[itemId2] = it'
+		its'.itemDB = its.itemDB ++ itemId -> it'
+		it'.name = its.itemDB[itemId].name
+		it'.count = plus[its.itemDB[itemId].count, quantity]
+	}
+}
+
+pred execute[] {
+	some disj its, its', its'': Inventory, itemId: ItemId, n: Name | {
+		init[its]
+		itemRegistration[its, its', itemId, 100, n]
+		receivingOrShipping[its', its'', itemId, -50]
+	}
+}
+
+run execute for 2 but 3 Inventory, 8 Int
+

モデルの可視化

+ 先ほどの InventoryManagement のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
+

+ この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
+ Inventory が，ItemId のインスタンスを Item のインスタンスに対応させる itemDB という + フィールドを持っており，Item が Name のインスタンスを参照する name フィールドと， + Int のインスタンスを参照する count フィールドを持っていることがわかります． +

InventoryManagement モデルの仮想実行について

+ ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+

仮想実行の可視化:

+ このテストケースはモデル中の execute 述語で実装されています．
+ execute の実行を可視化したものを以下に示します． +

+ 左下にある Inventory2($execute_its) は execute 述語中の変数 its で参照される Inventory のインスタンスであり，init 述語を満たしているため， + まだ何の商品(Item)も登録されていない状態になっています．
+ 次に，1番上の段の左にある Inventory1($execute_its') は変数 its' で参照される Inventory のインスタンスで， + its で参照される Inventory のインスタンスに対して，Item のインスタンス Item1(itemRegistration_it) を初期数量100個で登録したインスタンスになっています．
+ Inventory1 の右にあるInventory0($execute_its'') は少し複雑です．
+ まず，Inventory1 において，ItemId で参照される Item のインスタンスは Item1 です．このインスタンスに対して50個出荷した後の Item のインスタンスが Item0 になります．
+ ここで Item0 の在庫数が50個に減少していることに注意して下さい．
+ ItemId で参照される Item のインスタンスが Item1 から Item0 に変わるので，Inventory のインスタンスも Inventory1 から Inventory0 に変わります． +

+ 課題概要 +

+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある implies はその前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． +

+sig ItemId, Name{}
+sig Inventory {
+	itemDB: ItemId lone -> lone Item
+}
+sig Item {
+	name : Name,
+	count: Int
+}
+
+pred init[its: Inventory] {
+	no its.itemDB
+}
+
+pred itemRegistration[its, its': Inventory, itemId: ItemId, quantity: Int, n: Name] {
+	some it: Item |	{
+		no itemId2: ItemId | its.itemDB[itemId2] = it
+		its'.itemDB = its.itemDB + itemId -> it
+		it.name = n
+		it.count = quantity
+	}
+}
+
+pred shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: Int] {
+	plus[its.itemDB[itemId].count, quantity] < 0 implies {
+		all itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId']
+	}
+	else {
+		some it': Item | {
+			no itemId2: ItemId | its.itemDB[itemId2] = it'
+			its'.itemDB = its.itemDB ++ itemId -> it'
+			it'.name = its.itemDB[itemId].name
+			it'.count = plus[its.itemDB[itemId].count, quantity]
+		}
+	}
+}
+
+pred execute[] {
+	some disj its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {
+		init[its]
+		itemRegistration[its, its', itemId, 100, n]
+		shippingOrReceiving[its', its'', itemId, -50]
+		shippingOrReceiving[its'', its''', itemId, -75]
+	}
+}
+
+run execute for 2 but 4 Inventory, 8 Int
+

+ 【InventoryManagement(DTRAM) の課題】 +

+ ここでは，InventoryManagement の DTRAM による仕様記述に関する課題に取り組んでいただきます．
+ 以下に DTRAM で記述された InventoryManagement のモデルを示します．こちらを適宜参照しながら課題を進めてください． +

InventoryManagement の DTRAM による記述についての説明

+ DTRAMでは，InventoryManagement の仕様を以下のような階層化されたリソースで表します．
+

+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
+}
+

モデルの可視化

+ 先ほどの InventoryManagement のモデルのリソースとチャンネルを，DTRAM のモデリングツールを使用して可視化したものを以下の図に示します．
+

+ この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
+ 図の中央にある inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．
+ inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．
+ このリソース名に含まれる itemId は商品idを表すパスパラメータで，一意な商品の特定を可能にしています．
+ inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースは inventory.{itemId} の在庫数を表しており， + ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります． +

InventoryManagement モデルの仮想実行について

+ ここでは，InventoryManagement モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+

仮想実行の可視化:

+ シミュレーションツールを使用すると与えられたモデルに対して，任意の仮想実行を行うことができます．
+ ここでは上で示したテストケースに従って行った仮想実行を可視化したものを示していきます．まず，システムの初期状態を可視化したものが以下の図です． +

+ 初期状態では，inventory リソースには何の商品も登録されていない状態になっています．nil は空のマップやリストを表しています．
+ 次に，inventory に商品(Asahi)を登録するため，inventory リソースをダブルクリックします． +

+ registerItem という商品を登録するためのメッセージを選択します． +

+ registerItem メッセージのシグニチャが表示されます．
+ itemId は商品id，itemName は商品名，quantity は初期数量を表します． +

+ 次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つ商品 inventory.@123 が inventory の子リソースとして生成されていることがわかります．
+ inventory.@123 の在庫数量 inventory.@123.count が100，商品名 inventory.@123.name がAsahiとなっていることを確認できます．
+ 次に，登録した商品 inventory.@123 を50個出荷したいので，inventory.@123.count リソースをダブルクリックします． +

+ メッセージを選択する画面が同様に表示されますので，入荷か出荷を行う receiveOrShip というメッセージを選択します． +

+ 入荷数量，または出荷数量の入力が可能な画面が表示されますので，ここでは receiveOrShip(-50) と入力して実行します．
+ ここで quantity が正の値のときは入荷，負の値のときは出荷が行われます． +

+ 次の状態に遷移したため，inventory.@123.count リソースの状態が50に遷移したことが確認できました． +

+ 課題概要 +

+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った InventoryManagement の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． +

+channel ItemRegistration {
+	out inventory(itemDB:Map, registerItem(itemId:Str, itemName:Str, quantity:Int)) = insert(itemDB, itemId, {"count": quantity, "name": itemName})
+}
+
+channel Receiving(itemId:Str) {
+	out inventory.{itemId}.count(prev_quantity:Int, receive(quantity:Int)) = prev_quantity + quantity
+}
+
+channel Shipping(itemId:Str) {
+	out inventory.{itemId}.count(prev_quantity:Int, ship(quantity:Int)) = prev_quantity - quantity
+}
+
+

+ 【SimpleTwitter(Alloy) の課題】 +

+ ここでは，SimpleTwitter の Alloy による仕様記述に関する課題に取り組んでいただきます．
+ 以下に Alloy で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください． +

SimpleTwitter の Alloy による仕様記述についての説明

sig:

+ Alloy では，アカウントidの集合を AccountId，アカウント名の集合を Name， + ツイートの集合を Tweet，アカウントデータベースの集合を Accounts，アカウントの集合を Account，ツイートリストの集合を List で表します．
+ 以下のモデルでは sig を用いて，AccountId，Name，Tweet，Accounts，Account，List の順番にこれらの集合を宣言しています．
+ Accounts には，AccountId から Account への対応関係が accountDB フィールドとして定義されています．
+ ここで，AccountId の右側の lone は１つの Account に対応する AccountId がたかだか１つしかないことを示しています．
+ Account の宣言では，アカウント名を表す name が Name のインスタンスとして， + ツイートリストを表す tweets が List のインスタンスとして定義されています．
+ +

pred:

+ 最初の述語として記述されている init は，Accounts の + インスタンスである acs が初期化されていることを示しています．
+ 次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と， + 登録した後のインスタンス acs' の関係を述語として定義しています．ここで n はアカウント名を示しています．
+ また，述語定義中の some ac: Account は，acs のデータベースに登録されていない Account のインスタンス ac が存在していることを示しており， + 直観的には Account のインスタンスの生成を示しています．
+ tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と， + 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
+ 述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス ac' が存在していることを示しており， + 直観的には，Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
+ 最後の execute では，init，signUp，tweet をこの順で呼び出す操作を定義しています．
+ run では，execute を呼び出して仮想実行を行います． +

+sig AccountId, Name, Tweet { }
+sig Accounts {
+	accountDB: AccountId lone -> lone Account
+}
+sig Account {
+	name: Name,
+	tweets: List
+}
+
+sig List {
+	size: Int,
+	element: Int -> lone Tweet
+}
+
+pred init[acs: Accounts] {
+	no acs.accountDB
+}
+
+pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
+	some ac: Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac
+		acs'.accountDB = acs.accountDB + id -> ac
+		ac.name = n
+		ac.tweets.size = 0
+		no ac.tweets.element
+	}
+}
+
+pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
+	some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = acs.accountDB[id].name
+		ac'.tweets != acs.accountDB[id].tweets
+		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
+		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
+		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
+	}
+}
+
+pred execute[] {
+	some disj acs, acs', acs'': Accounts, id: AccountId, n: Name, contents: Tweet | {
+		init[acs]
+		signUp[acs, acs', id, n]
+		tweet[acs', acs'', id, contents]
+	}
+}
+
+run execute for 2 but 3 Accounts
+

モデルの可視化

+ 先ほどの SimpleTwitter のモデルの構造を，Alloy の可視化ツールを使用して可視化したものを以下の図に示します．
+

+ この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
+ Accounts が，AccountId のインスタンスを Account のインスタンスに対応させる accountDB というフィールドを持っており， + Account が Name のインスタンスを参照する name フィールドと，List のインスタンスを参照する tweets フィールドを，
+ List が Int のインスタンスを参照する size フィールドと， + Int のインスタンスを Tweet のインスタンスに対応させる element フィールドをもっていることがわかります． +

SimpleTwitter モデルの仮想実行について

+ ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+

仮想実行の可視化:

+ このテストケースはモデル中の execute 述語で実装されています．
+ execute の仮想実行を可視化したものを以下に示します． +

+ 左下にある Accounts2($execute_acs) は execute 述語中の変数 acs で参照される Accounts のインスタンスであり，init 述語を満たしているため， + まだ何のアカウント(Account)も登録されていない状態になっています．
+ 次に，1番上の段の左にある Accounts1($execute_acs') は変数 acs' で参照される Account のインスタンスで， + acs で参照される Account のインスタンスに対して，Account のインスタンス Account1($signUp_ac) をツイートリストの要素数が0の状態で登録したインスタンスになっています．
+ Accounts1 の右にある Accounts0($execute_acs'') は少し複雑です．
+ まず，Accounts1 において，AccountId で参照される Account のインスタンスは Account1 です．このインスタンスに対してツイートを行った後の Account のインスタンスは Account0 になります．
+ ここで Account0 のツイートリストの要素数が1に増加していることに注意して下さい．
+ AccountId で参照される Account のインスタンスが Account1 から Account0 に変わるので，Accounts のインスタンスも Accounts1 から Accounts0 に変わります． +

+ 課題概要 +

+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ なお，以下のモデル中にある implies はその前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． +

+sig AccountId, Name, Tweet { }
+sig Accounts {
+    accountDB: AccountId lone -> lone Account
+}
+sig Account {
+    name: Name,
+    tweets: List
+}
+
+sig List {
+    size: Int,
+    element: Int -> lone Tweet
+}
+
+pred init[acs: Accounts] {
+    no acs.accountDB
+}
+
+pred signUp[acs, acs': Accounts, id: AccountId, n: Name] {
+	some ac': Account | acs.accountDB[id] = ac' implies {
+		all id': AccountId | acs'.accountDB[id'] = acs.accountDB[id']
+	}
+	else {
+		some ac: Account | {
+			no id2: AccountId | acs.accountDB[id2] = ac
+			acs'.accountDB = acs.accountDB + id -> ac
+			ac.name = n
+			ac.tweets.size = 0
+			no ac.tweets.element
+		}
+	}
+}
+
+pred tweet[acs, acs': Accounts, id: AccountId, contents: Tweet] {
+    some ac': Account | {
+		no id2: AccountId | acs.accountDB[id2] = ac'
+		acs'.accountDB = acs.accountDB ++ id -> ac'
+		ac'.name = acs.accountDB[id].name
+		ac'.tweets != acs.accountDB[id].tweets
+		ac'.tweets.size = plus[acs.accountDB[id].tweets.size, 1]
+		ac'.tweets.element[minus[ac'.tweets.size, 1]] = contents
+		all n: Int | n != minus[ac'.tweets.size, 1] implies ac'.tweets.element[n] = acs.accountDB[id].tweets.element[n]
+	}
+}
+
+pred execute[] {
+	some disj acs, acs', acs'', acs''': Accounts, id: AccountId, disj n, n': Name, contents: Tweet | {
+		init[acs]
+		signUp[acs, acs', id, n]
+		signUp[acs', acs'', id, n']
+		tweet[acs'', acs''', id, contents]
+	}
+}
+
+run execute for 2 but 4 Accounts
+

+ 【SimpleTwitter(DTRAM) の課題】 +

+ ここでは，SimpleTwitter の DTRAM による仕様記述に関する課題に取り組んでいただきます．
+ 以下に DTRAM で記述された SimpleTwitter のモデルを示します．こちらを適宜参照しながら課題を進めてください． +

SimpleTwitter の DTRAM による記述についての説明

+ DTRAM では，SimpleTwitter の仕様を以下のような階層化されたリソースで表します．
+

+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)
+}
+

モデルの可視化

+ 先ほどの SimpleTwitter のモデルのリソースとチャンネルを，DTRAM のモデリングツールを使用して可視化したものを以下の図に示します．
+

+ この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
+ 図の中央にある accounts リソースは Signup チャンネルからアカウントを登録するメッセージを受け取ります．
+ accounts リソースの子リソースである，accounts.{accountId} リソースはアカウントを表しています．
+ このリソース名に含まれる accountId はアカウントidを表すパスパラメータで，一意なアカウントの特定を可能にしています．
+ accounts.{accountId} リソースの子リソースである accounts.{accountId}.tweets リソースは accounts.{accountId} のツイートリストを表しており， + Tweet チャンネルからツイートを行うメッセージを受け取ります． +

SimpleTwitter モデルの仮想実行について

+ ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．
+

仮想実行の可視化:

+ 初期状態では，accounts リソースには何のアカウントも登録されていない状態になっています．
+ 次に，accounts にアカウント名が "Satou" のアカウントを登録するため，accounts リソースをダブルクリックします． +

+ signUp というアカウントを登録するためのメッセージを選択します． +

+ signUp メッセージのシグニチャが表示されます．
+ accountId はアカウントid，name はアカウント名を表します． +

+ 次の状態に遷移し，遷移後の状態が表示されます．@123というidを持つアカウント accounts.@123 が accounts の子リソースとして生成されていることがわかります．
+ accounts.@123 のツイートリスト accounts.@123.tweets が空のリスト(nil)，アカウント名 accounts.@123.name が "Satou" となっていることを確認できます．
+ 次に，登録したアカウント accounts.@123 でツイートを行いたいので，accounts.@123.tweets リソースをダブルクリックします． +

+ メッセージを選択する画面が同様に表示されますので，ツイートを行う tweet というメッセージを選択します． +

+ ツイート内容の入力が可能な画面が表示されますので，ここでは tweet("Hello") と入力して実行します．
+

+ 次の状態に遷移したため，Hello というツイート内容を持つツイート accounts.@123.tweets.0 が accounts.@123.tweets の子リソースとしてツイートリストの0番目に生成されていることが確認できました． +

+ 課題概要 +

+ ここからが課題です．
+ 本課題ではまず，上記にて説明を行った SimpleTwitter の仕様に，ある機能を追加した仕様を考えます．
+ その仕様のモデルを以下に示します．また，そのモデルの仮想実行を可視化したものをその下に示します．これらの図を見ていただいた上で，２つの設問にお答えいただきます．
+ 設問にお答えいただく際は，必ず設問１，設問２の順番でご解答下さい．以下の図と同じものが設問のページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません． +

+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)
+}
+
+channel ChangeName(accountId:Str) {
+	out accounts.{accountId}.name(prevNamr:Str, changeName(name:Str)) = name
+}
+
+
+

+ 【InventoryManagement(Alloy) の課題】 +

InventoryManagement の Alloy による仕様記述についての説明

`sig`:

`pred`:

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

+ 【InventoryManagement(DTRAM) の課題】 +

InventoryManagement の DTRAM による記述についての説明

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

1:

2:

3:

4:

5:

6:

7:

+ 【SimpleTwitter(Alloy) の課題】 +

SimpleTwitter の Alloy による仕様記述についての説明

`sig`:

`pred`:

モデルの可視化

SimpleTwitter モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

+ 【SimpleTwitter(DTRAM) の課題】 +

SimpleTwitter の DTRAM による記述についての説明

モデルの可視化

SimpleTwitter モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

1:

2:

3:

4:

5:

+ 【InventoryManagement(Alloy) の課題】 +

InventoryManagement の Alloy による仕様記述についての説明

sig:

pred:

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

+ 【InventoryManagement(DTRAM) の課題】 +

InventoryManagement の DTRAM による記述についての説明

モデルの可視化

InventoryManagement モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

1:

2:

3:

4:

5:

6:

7:

+ 【SimpleTwitter(Alloy) の課題】 +

SimpleTwitter の Alloy による仕様記述についての説明

sig:

pred:

モデルの可視化

SimpleTwitter モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

+ 【SimpleTwitter(DTRAM) の課題】 +

SimpleTwitter の DTRAM による記述についての説明

モデルの可視化

SimpleTwitter モデルの仮想実行について

仮想実行の可視化:

+ 課題概要 +

1:

2:

3:

4:

5:

`sig`:

`pred`:

`sig`:

`pred`: