Fork: 0
nitta-lab / SpecificationSimulatorExperiments
Transfer to URL with SHA Find file
Newer
Older
SpecificationSimulatorExperiments / courseA / IM_Alloy.html
okazakitakehiro 15 days ago 10 KB IM_Alloyが完成．
Raw Blame History 
<!DOCTYPE html>
<html lang="ja">
<head>
    <meta charset="UTF-8">
	<style>
		c1{
			color: blue;
		}
		c2{
			color: red;
		}

	</style>
    <title>【InventoryManagement(Alloy)】</title>
</head>
<body>
<h1 class="title">
	【InventoryManagement(Alloy)の課題】
</h1>
<p>
	ここでは，InventoryManagementのAlloyによる仕様記述の課題に取り組んでいただきます．<br>
	以下にAlloyで記述されたInventoryManagementのモデルを示します．こちらを適宜参照しながらモデルの理解を行ってください．
</p>
<hr/>

<h2>InventoryManagementのAlloyによる記述についての説明</h2>
<h3><code><c1>sig</c1></code>:</h3>
<p>
	以下のモデルでは始めに，商品IDの集合を表す <code>ItemId</code> と商品名の集合を表す <code>Name</code> を宣言しています．<br>
	次に，商品全体を保管する倉庫の集合を表す <code>Inventory</code> を宣言しています．<code>Inventory</code> には，<code>ItemId</code> から
	商品情報を表す <code>Item</code> への対応関係が<code>itemDB</code> フィールドとして定義されています．<br>
	最後の <code>Item</code> では，商品名を表す <code>name</code> が <code>Name</code> のインスタンスとして，
	在庫数を表す <code>count</code> が <c2><code>Int</code></c2> のインスタンスとして定義されています．<br>
</p>

<h3><code><c1>pred</c1></code>:</h3>
<p>
	最初の述語として記述されている <code>init</code> は，<code>Inventory</code> の
	インスタンスである <code>its</code> が初期化されているという条件を満たしていることを示しています．<br>
	次の，<code>itemRegistration</code> は <code>itemId</code> で示された商品を登録する前の <code>Inventory</code> のインスタンス <code>its</code> と
	登録した後のインスタンス <code>its'</code> の関係を述語として定義しています．<br>
	ここで <code>quantity</code> は初期数量，<code>n</code> は商品名を示しています．<br>
	<code>receivingOrShipping</code> では<code>itemId</code> で登録されている商品に対して
	入荷か出荷を行った際の操作前の <code>Inventory</code> のインスタンス <code>its</code> と操作後のインスタンス <code>its'</code> の関係を述語として定義しています．<br>
	ここで <code>quantity</code> が正の値のときは入荷，負の値のときは出荷を表しています．<br>
	最後の <code>execute</code> では，<code>init</code> ，<code>itemRegistraction</code> ，<code>receivingOrShipping</code> を
	この順で呼び出す操作を定義しています．<br>
	<c1><code>run</code></c1> では，<code>execute</code> を呼び出して実行を行います．
	この実行の際に，<code>Int</code> で8bitの数字を扱うことができるよう末尾に <code><c2>8</c2></code>  <code><c1>Int</c1></code> という記述を行っています．
</p>

<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
	<pre>
<c1>sig</c1> ItemId, Name{}
<c1>sig</c1> Inventory {
	itemDB: ItemId <c1>lone</c1> -> <c1>lone</c1> Item
}
<c1>sig</c1> Item {
	name : Name,
	count: <c1>Int</c1>
}

<c1>pred</c1> init[its: Inventory] {
	<c1>no</c1> its.itemDB
}

<c1>pred</c1> itemRegistration[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>, n: Name] {
	<c1>some</c1> it: Item | {
	<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it
	its'.itemDB = its.itemDB + itemId -> it
	it.name = n
	it.count = quantity
	}
}

<c1>pred</c1> receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] {
	<c1>some</c1> it': Item | {
	<c1>no</c1> 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]
	}
}

<c1>pred</c1> execute[] {
	<c1>some disj</c1> its, its', its'': Inventory, itemId: ItemId, n: Name | {
    	init[its]
    	itemRegistration[its, its', itemId, <c2>100</c2>, n]
    	receivingOrShipping[its', its'', itemId, -<c2>50</c2>]
	}
}

<c1>run</c1> execute <c1>for</c1> <c2>2</c2> but <c2>3</c2> Inventory, <c2>8</c2> <c1>Int</c1>
	</pre>
</div>
<hr/>

<h2>モデルの可視化</h2>
<p>
	先ほどのInventoryManagementのモデルの構造を，Alloyの可視化ツールを使用して，可視化したものを以下の図に示します．<br>
</p>
<div class="img-center">
	<img src="../img/Alloy/Alloy MetaModel Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
	この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．<br>
	<code>Inventory</code> が，<code>ItemId</code> のインスタンスを <code>Item</code> のインスタンスに対応させる <code>itemDB</code> という
	フィールドを持っており，<code>Item</code> が <code>Name</code> のインスタンスを参照する <code>name</code> フィールドと，
	<code>Int</code> のインスタンスを参照する <code>count</code> フィールドを持っていることがわかります．
</p>
<hr/>

<h2>InventoryManagementモデルの仮想実行について</h2>
<p>
	ここでは，InventoryManagementモデルの仮想実行について説明します．InventoryManagementの仮想実行で用いるテストケースは次の通りです．<br>
	<ol>
	<li>Inventoryに新しく取り扱う商品を初期数量100で登録します．</li>
	<li>登録した商品を50個出荷します．</li>
	</ol>
</p>

<h3>仮想実行の可視化:</h3>
<p>
	このテストケースはモデル中の <code>execute</code> 述語で実装されています．<br>
    <code>execute</code> の仮想実行を可視化したものを以下に示します．
</p>
<div class="img-center">
	<img src="../img/Alloy/Alloy Ver InventoryManagement.png", class ="before-image-size"><br>
</div>
<p>
	左下にあるInventory2($execute_its)は <code>execute</code> 述語中の変数 <code>its</code> で参照される <code>Inventory</code> のインスタンスであり，
	<code>init</code> 述語を満たしているため，まだ何の商品(Item)も登録されていない状態になっています．<br>
	次に，1番上の段の左にあるInventory1($execute_its')は変数 <code>its'</code> で参照されるインスタンスで，
	<code>its</code> で参照されるインスタンスに対して <code>itemId</code> で参照される <code>Item</code> のインスタンスを初期数量100個で登録したインスタンスになっています．<br>
	そして，Inventory1の右にあるInventory0($execute_its'')は<code>itemId</code> で参照される <code>Item</code> のインスタンスを50個出荷したインスタンスになっているため，
	在庫数が50個に減少しています．<br>
	ここで出荷前の <code>Item</code> のインスタンス(Item1)と出荷後のインスタンス(Item0)が別々のインスタンスになっていることに注意して下さい．<br>
</p>
<hr/>

<h2>
	課題概要
</h2>
<p>
	本課題ではまず，上記にて説明を行ったInventoryManagementに，ある機能を追加したモデルとその仮想実行を可視化した以下の図を見ていただき，
	２つの設問に答えていただきます．<br>
	必ず設問１，設問２の順番でご解答下さい．<br>
	以下の図は設問のページにも記載されているページにも記載されているのでこのまま設問のページに飛んでいただいてもかまいません．
</p>
<div style="padding: 10px; margin-bottom: 10px; border: 1px solid #333333; border-radius: 10px;">
<pre>
<c1>sig</c1> ItemId, Name{}
<c1>sig</c1> Inventory {
	itemDB: ItemId <c1>lone</c1> -> <c1>lone</c1> Item
}
<c1>sig</c1> Item {
	name : Name,
	count: <c1>Int</c1>
}

<c1>pred</c1> init[its: Inventory] {
	<c1>no</c1> its.itemDB
}

<c1>pred</c1> itemRegistration[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>, n: Name] {
	<c1>some</c1> it: Item |	{
	<c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it
    	its'.itemDB = its.itemDB + itemId -> it
    	it.name = n
		it.count = quantity
	}
}

<c1>pred</c1> shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] {
	plus[its.itemDB[itemId].count, quantity] < <c2>0</c2> <c1>implies</c1> {
		<c1>all</c1> itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId']
	}
	<c1>else</c1> {
		<c1>some</c1> it': Item | {
		<c1>no</c1> 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]
		}
	}
}

<c1>pred</c1> execute[] {
	<c1>some disj</c1> its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {
	init[its]
	itemRegistration[its, its', itemId, <c2>100</c2>, n]
	shippingOrReceiving[its', its'', itemId, -<c2>50</c2>]
	shippingOrReceiving[its'', its''', itemId, -<c2>75</c2>]
	}
}

<c1>run</c1> execute <c1>for</c1> <c2>2</c2> <c1>but</c1> <c2>4</c2> Inventory, <c2>8</c2> <c1>Int</c1>
</pre>
</div>

<div class="img-center">
	<img src="../img/Alloy/Alloy_Ver_InventoryManagementCheckMinus.png", class ="before-image-size"><br>
</div>

<p>
	<strong>
		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf5rIUfHnzsLMLPZ_KWnsukn3HcEGBSLN-BxzRPzqszyrlj8g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
			課題アンケート (別タブが開きます)
		</a>
	</strong>
	<br>
	<strong>
		<a href="https://docs.google.com/forms/d/e/1FAIpQLSf8Ex1RPzMRvyUYIRkCjcIY69fI74sNXK-m4rNAoAcR6_dm4g/viewform?usp=sf_link" target="_blank" rel="noopener noreferrer">
			課題終了後の評価アンケート (別タブが開きます)
		</a>
	</strong>
</p>

<hr>
<br>
<a href="IM_DTRAM.html">【InventoryManagement(DTRAM)】へ</a>
</body>

<style>
	.title{
		text-align: center;
	}
	.links-manual-A{
        display: flex;
        flex-direction: column;
    }
    .img-center{
    	display: flex;
    	justify-content: center;
    	align-items: center;
    }
    .before-image-size{
        max-width: 100%;
        height: auto;
    }
    .after-image-size{
        max-width: 100%;
        height: auto;
    }
</style>

</html>