Philipz學習日誌

Hello all
I am a new HUGO/RT user. I am having problems to retranslate UML runs from SPIN trails. Your support would be appreciated to solve this matter. Here are the details of my tests:

1.- I initially modelled a simple set of state charts with ArgoUML (prenoms.zargo)
2.- As suggested by hugo/rt documentation, I preferred to work with the UTE model representation (prenoms.ute) to which I added an "empty" collaboration and object definition so that HUGO/RT could generate useful PROMELA code (prenoms.pr)
3.- Making use of XSPIN, I generated a simple trail (renamed as prenoms.tl) with the PROMELA specification and a simple LTL formula
4.- I tried the following command to retranslate the spin trail into a dot spec, as you can see I had no success: java -jar hugort.jar -odot=prenoms.dot prenoms.tl prenoms.ute
This is the output I got:
Hugo/RT v0.42, 05/02/02
Parsing UML model from `prenoms.ute'...
Checking UML model `Tequila'...
Writing dot to `prenoms.dot'...
Translating collaboration `empty' in UML model `Tequila' into UPPAAL...
Parsing UPPAAL trail from `prenoms.tl'...
[ERROR] Trail parsing failed: Encountered "-" at line 1, column 1.
Was expecting:
"State:" ...

If more details are needed, please, do not hesitate to let me know.

Kind regards,
Javier

Posted by Javier Rubio-Loyola at May 31, 2005 01:55 AM

Javier,

I am very happy you find this page about Hugo/RT.
Actually, Hugo/RT still has some bugs when you translate to SPIN promela language.
I also had the same problem.
If you can email to me the UTE file or ArgoUML file, maybe I will clear understand where the problem is.

Below is Hugo/RT Author, Alexander, answered my question about this translator on SPIN.

Dear Philipz,

here is the detailed procedure using the atm.ute example of the
distribution:

1. Translate the model with an assertion (or interaction) into Promela:

./hugort -opromela=output/atm.spin -c -a=sanity models/atm.ute

This produces in particular a file

output/atm.spin.ltl

which contains a temporal logic formula, here:

> ((term) && (term_G5))

2. Translate the temporal logic formula of output/atm.spin.ltl into a SPIN
never claim:

spin -f "> ((term) && (term_G5))"

This produces the never claim on the console.

3. Copy the never claim into output/atm.spin.ltl in between the lines
starting with "#define" and the line starting with "#ifdef NOTES":

#define term_G5 (Bank[processIds[obj_bank-1]]:state4 == VerifyingCard)
#define term (Bank[processIds[obj_bank-1]]:numIncorrect == 2)

never { /* > ((term) && (term_G5)) */
T0_init:
if
:: ((term) && (term_G5)) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}

#ifdef NOTES
> ((term) && (term_G5))
#endif

4. Translate the Promela code and the never claim into C:

spin -a -N output/atm.spin.ltl output/atm.spin

This produces a file named "pan.c".

5. Translate the C code for the model checker:

gcc -DNOREDUCE -o pan pan.c

The definition of NOREDUCE is necessary because of variable references in
the never claim.

6. Check the model:

./pan

This produces a trail file named "atm.spin.trail"

7. Translate the trail file into a readable format:

spin -l -g -w -v -t output/atm.spin > output/atm.tl

8. Retranslate the readable SPIN trail file into the notions of UML:

./hugort -otrail=output/atm.utl -c -a=sanity output/atm.tl models/atm.ute

Step 2-6 may be more easily done using XSPIN. And, yes, this calls for some
script...

Caveat: There is an error in the Hugo/RT 0.41 version: In order to
reconstruct UML from SPIN trails it is necessary to remove all lines after
the line "spin: trail ends after steps". I've put a corrected
version (Hugo/RT 0.42) on the web site.

Hope this helps,
Best regards,
Alexander.

Posted by philipz at May 31, 2005 03:53 AM

Dear Philipz,
Thanks for your quick answer, I will follow Alexander's suggestions right away.
I will be happy to e-mail you my files, please give me your address, haven't found it in this page.

Regards,
Javier

Posted by Javier Rubio-Loyola at May 31, 2005 05:50 PM

Dear Javier

My Email address is philipzheng@gmail.com
Hope you solve this problem successfully.

Sincerely,
Philipz

Posted by philipz at May 31, 2005 06:31 PM

Dear Philipz,
找Model Checking相關的資訊
發現貴Blog有這篇相當不錯的介紹
不過在轉換ute時發生了點問題
所以想請教一下您在使用ArgoUML時
State Diagram與Class的宣告之類都寫的很嚴謹嗎,
或是只寫個虛擬碼之類的就能轉
感謝您

Posted by Kividy at June 6, 2006 10:32 PM

Dear Kividy,
很高興看到您留言。
關於ArgoUML透過Hugo/RT轉換成Model Checking的語言
不建議直接轉換，的確先轉成中間格式UTE是比較好的
之後還是必須依照Hugo/RT的網站上說明再稍微修改UTE以便符合您所要轉換的語言。
Hugo/RT對於ArgoUML有版本支援的問題，那一版比較好，小弟已經忘記了。
希望這對您有幫助。
順道一提，剛好月初時，用到這Model Checking來驗證UML的論文
Constraint-Based Software Specifications and Verification Using UML
恰好剛刊登出來。

Posted by philipz at June 6, 2006 10:51 PM

Dear Philipz,
感謝您的回答
我大概了解了
我想我得先解決ArgoUML太難用這個問題
因為在轉成ute時都無法成功了
感謝您

Posted by Kividy at June 6, 2006 11:37 PM

Dear Philipz,
我是您實驗室學弟 聖瑜,
最近因論文需要在做Model Checking,
參考了您的文章及論文,
發生了些問題想請教一下,
collaboration看例子上來說是atm及bank間的一些關係,
若我今天只有單一一個class的話能夠用collaboration
來描述assertion的關係嗎?
因為我要驗證的其中一個model剛好跟atm及bank的兩次錯誤的驗證相同,但是我只有單一個class,
且在用uppaal驗證時一直告訴我Syntax Error,
好像是什麼Declaration裡有個ID的Syntax Error,
不知道跟上面的問題有沒有關,
麻煩學長指教一下,thank you.

Posted by Stanely at June 8, 2006 04:40 PM

不好意思連發兩篇
不知道uppaal您有沒有當初您在用時的版本
因為我目前用最新版試著去驗証
Hugo/RT本身提供的例子也會發生錯誤
如果有的話不知道可不可以麻煩您寄給我或老師
謝謝您

Posted by Stanely at June 8, 2006 05:40 PM

聖瑜：

只有一個class應該沒法模擬出atm及bank間的關係，應該要兩個class才可以。
uppaal我當時使用的版本，已經忘記是那一個了，也沒有保留，所以可能沒法傳給你。
你可能要上Hugo/RT網站研究一下那語法，可能對你有幫助，轉成UTE檔後，再修改，應該就可以。

Posted by philipz at June 9, 2006 12:10 AM

Dear Philipz,
看來也只能這樣子了,
我再研究研究看看好了,
謝謝您呀^^

Posted by Stanely at June 12, 2006 03:15 PM

用uppaal,editor编辑的系统状态转移图，怎么转换到word里呢？非常感谢你！

Posted by susan at March 2, 2007 08:12 PM

Susan,

用Print Screen就可以貼到Word上面去了。

Posted by philipz at March 2, 2007 08:55 PM

非常感谢，祝你节日快乐！

Posted by susan at March 4, 2007 05:23 PM

Name:


Email Address:


URL:



請依上圖輸入檢核碼：

Remember personal info?
YesNo
Comments: