All posts by hevangel

加拿大洛磯山脈自駕遊(一) – 哥倫比亞冰原

說來慚愧,我在加拿大卑詩省住了十多年,竟然還沒有去過風光如畫,旅遊加西指定景點的班芙國家公園(Banff National Park)。今年暑假趁阿仔未入學前,一家人開車展開十天九夜,從卑詩省一直玩到阿省,超過二千五百公里的長征旅行。這次個多星期的road trip,相信是我有生以來駕車最多的日子。除了逗留在班芙那幾天,每天都開車前住新的城市,回程時平均每天開車五六小時。幸好老婆有幫手開車,阿仔也要途中停車休息玩耍,加上穿州過省的登山公路景色優美,開長途車也不至於太過辛苦。不過每天開五六小時已是極限,很難想像有些人可以一口氣連開十多小時車,一天內從溫哥華直達班芙。

Road Trip開車雖然辛苦,但比起巴士團勝在自由度高,喜歡在那裏停多久玩多久也行,又不用被迫參觀無聊的景點浪費時間。很多人去班芙國家公園會選擇露營,不過因為阿仔年紀還小,加上是第一次開長途車旅行,寧願貴點住得酒店住得舒服些。阿仔第一次坐長途車,所以從溫哥華到班芙的路程分開三天。第一天住宿距離三小時車程的小鎮Merrit,基本上該小鎮沒有任何值得一看的景點,除了逛逛市中心那兩條街外,就只有吃飯睡覺,鈰上勉強有個鄉郊音樂節的展覽館,不過我不懂鄉郊音樂,對此完全沒有輿趣。第二天開車到卑詩省第三大城市Kelowna,是省內著名的酒鄉,湖畔兩岸有很多大小酒莊和哥爾夫球場,是輕鬆旅行渡假的好去處。早幾年有朋友在那兒結婚曾到此一遊,不妨看看舊文卑詩內陸酒鄉遊的介紹。今次純萃路過借宿一宵,只帶阿仔到市中心公園玩耍放電,沒有時間去什麼地方觀光。

Kelowna市中心公園
沿湖公路北上

從Kelowna到Banff北上走一號橫加公路車程五個半小時,途經Venon,Revelstoke,Golden等小鎮。連同中途停下來吃午飯,休息歇腳,上洗手間的時間,早上吃過早餐後開車,要到晚餐時份才抵達班芙,差不多開了一整天車。享受駕駛樂趣的朋友,必定喜歡開這段橫加公路。與平時在城市中開車整天要停紅綠燈,塞車煩人完全不同,在郊外的道路上開車暢通無阻,可以讓人隨心所欲地在馬路上飛馳。沿著河谷的公路登山而上,橫越海拔五千尺的磯山脈,看著兩旁高聳積雪的山峰,夾谷連綿不絕的綠色森林,時而大直路時而急轉灣,在超車線加速至時速一百四十公里,一口氣超越前面慢行的大貨車,那才是享受駕駛應有的感覺。愛好攝影的朋友,公路沿途有很多景點停車位,可以飽覽國家公園的湖光山色。沿途有一件小插曲,近日卑詩省天氣乾燥山火嚴重,橫加公路其中一段也有小規模山火,當然沒有滿山紅紅的火焰,不然早就封路了,但可以看見山腰有數處冒煙。最難得剛巧看見消防直升機吊著水彈來救火,平時阿仔讀故事書看得多,第一次親眼見到消防直升機十分興奮,可惜我在駕車沒法分心拍照。

聖路易斯湖如鏡的倒影
青藍色的湖水

班芙國家公園是加拿大首個國家公園,原本班芙只是橫加鐵路中途的一個補給站,洛磯山風景優美令很多旅客慕名前來,漸漸發展成一個夏天登山遠足露營看野生動物,冬天滑雪浸溫泉的渡假勝地。我不是攝影發燒友,去旅行只是手機隨便影相,不過班芙國家公園肯定會令風影攝影龍友著迷。洛磯山脈連綿不絕的高山,因為不同地質風化程度不同,山頂的岩峰各有特色,有些像金字塔,有些像堡壘,蔚為奇觀。不少高峰更是終年積雪,與山與山之間峽谷的原始森林,相映成趣。山頂溶了的雪水住下流薈聚成河,分別流向大陸兩岸的大西洋和太平洋。雪水顏色特別青藍亮麗,湖水平靜如鏡影照山峰的倒影,在太陽光照下閃閃生輝,如畫般的山與水。

哥倫比亞冰原,中央的小黑點是怪獸巴士
怪獸巴士

班芙最著名的景點是哥倫比亞冰原,面積有三百平方公里(大約等於四個香港島的大小),積雪最深厚達三百五十米,自史前冰河時期以來從未融化。嚴格來說冰原位並不屬於班芙國家公園的笵圍,而是位於Jasper國家公園之內,兩個國家公園雙連接,而從班芙開車去冰原比Jasper近些,大約只要兩個半小時。我們選擇坐從班芙出發即日來回的Brewster巴士團,與登上冰川的怪獸巴士是同一間公司,雖然自已駕車去冰川然後購怪獸巴士票會便宜些少,但巴士團一條龍服務免卻排隊的煩麻。巴士沿途例牌停幾個景點讓遊客拍照鬆腳,車上導遊解班芙國家公園的歷史和趣事,這些故事自己駕車去就聽不到。我們的導遊更是打暑期工的讀地理大學生,秀知識給我們上了一堂地理課,淺白地講解不同岩石如何形成不同形狀的山峰,增長了不少冷知識。團費還包括一頓不錯的西式自助餐,在冰原旅客中心的餐廳邊看冰川邊吃,吃完直接登山舒服省時。

踏足冰川

從旅客中心望過去,看不出冰川有多巨大,還因為冰川有一小半融化了,露出峽谷兩旁的岩石,我還有點兒看輕它。只不過是五十年前,冰川還是從山頂一直申延到公路旁,因為溫室效應全球暖化,冰川以每年五十米的速度融化,若果碳排放沒有改善,過多幾十就再看不到冰川了。普通汽車沒法駛上冰川,更不要說徙步登上去,我們轉乘坐每台造價百萬美元的特制雪地怪獸巴士。怪獸巴士緩緩駛進冰川,我才感受到冰川的巨大,山峽兩旁的岩石不是簡單的融冰後露出來,而是被冰川流過巨大的力量,把岩石整齊地砌開來。我們參觀那天日光普照,氣溫有二十五度,冰川上不是太冷,大在約十度左右,只是下降了十五度,著長袖衫加件風褸就可以。怪獸巴士駛到冰川一半左右,放旅客下車有二十分鐘自由活動時間。踏足冰川就好像在一個凹凸不平的溜冰場,要很小心行路不然很容易滑倒。冰川上最重要的活動是拍照,鏡頭除了對準冰川本身,冰川盡頭處冰原,兩旁山峰的小冰川外,不少遊客還與怪獸巴士合照,畢竟那是非常罕見的交通工具,全世界只有兩個地方有雪地怪獸巴士坐,其一處是這兒,另一處是冰島。落車時導遊派你一個水杯,用來裝冰川水喝。喝冰要水走到安全線內的最高點,在沒有其他人行走留下污染的地方,彎下身用杯子瓢起從冰原流下來的冰川水。冰川水味道清純冰涼,老實說與雪凍了的礦泉水沒有什麼分別,不過我總算是喝過了。

玻璃橋

買豬肉送豬頭骨,看完冰川下山後,巴士團繼續前住下一個景點玻璃橋,也是怪獸巴士同一間公司經營。近年不少地方也興建同類玩意,美國大峽谷有,中國張家界也有,有峽谷的地方就有。你問我玻璃橋有什麼特別,只是看風景拍照的話,與停在馬路旁看沒有分別。宣傳廣告說什麼凌空漫步,體驗峽谷的驚險高度,我完全感覺不到。從玻璃橋向下望是很高,但肯定高不過百多層樓摩天大廈。若果不是跟團的話,玻璃橋可以不用去,自費入場可要三十多元,不值。看完冰川和玻璃橋,回程時大半車人都累得睡著了,回到班芙市已是晚飯時間,一天的冰川之旅美滿地完結。想看冰川就要趁早了,再過多十幾二十年,冰川融化後便就沒有得看了。

Alien: Covenant 異形:聖約

人類創造人造人,人造人創造異形。這套《異形》前傳的續集,終於解開異形起源之謎。上集《普羅米修斯》故弄玄虛,令我對這套《異形:聖約》沒有抱多大期望。不過身為多年的異形老影迷,既然Ridley Scott繼續拍,我自然要繼續捧場。其實單看片名,便知今集雷度高。還以為聖約會是什麼新東西?原來只是一艘太空殖民船的名字。太空船的名字隨得你改,編劇喜歡叫什麼也行,改這個令人充滿聯想的名字,分明想誤導觀眾。不過上集的戲名也是用太空船的名字,算是某種一默相承吧。

說起一默相承,這集太空船的船員與上集同樣低能白痴,所有船員的行動非常兒戲,沒有計劃亂衝亂撞,完全不像受過嚴格訓練的太空人。明明只要僅守探險安全守則,先在軌道上派無人機作偵測,確定安全探險隊員才下降,便不會落得全軍盡默的下場。又不是很趕時間,為什麼急著登陸去送死?上半場非常沉悶,太空船遇到電磁風暴,電腦把船員從冬眠倉喚醒,不知何解船長的冬眼倉會著火,殺了他讓白痴二副坐正當新船長。在太空中偶然接收到音樂廣播,巧合地訊號來自一顆走漏眼的可居住地球,於是大家便放棄原本的殖民任務,走去這個新發現一無所知的星球。就算沒有遇到異形一切順利,其他冬眠的殖民者醒來,發現目的地無端端改變了,不知他們可否要回水。

終於等到異形出場,異形擒臉生蛋爆肚出世,總算有點回到初代的感覺。最初出場的異形是未完成品,破壞力十分有限,機關槍也可以殺死牠。上集的人造人今集改行做奸佬,飛了去外星人的母星先用生化武器殺光他們,然後留下來研究新物種創造異形。有兩點我不明白,為什麼人造人的頭髮會生長,又為什麼外星人完全不似擁有高度文明。他們有能力建創太空船創造人類,居住的地方卻像古希臘。大慨美術指導只求外星人城市宏偉好看,完全沒有考慮與劇中科技程度是否配合。異形出場後的劇情十分《異形》公式,異形同隊員玩逐個捉,觀眾估不到攘下來誰會死,不過肯定最後全部領便當。結局女主角大顯神威連打兩次異形,第一次在登陸艇用機械臂打異形,然後異形不知怎樣偷渡上太空船,於是又打多一次掉牠出太空。女主角成套戲行行企企,還以為她只是個花瓶,最後打異形時身手尚可,不過始終與薜歌妮韋花終於差幾皮。

Ridley Scott明言《異形》系列長拍長有,今集結尾當然要留伏筆。伏筆非常容易估,兩個人造人相貌相同,當然是用來調包嘛。不過我不明白David為什麼不索性殺掉女主角和肥佬,又或控制門鎖者讓異形吃掉他們,何需要一直扮Walter騙他們回去冬眠呢。我對今集《異形:聖約》完全沒有任何期望,所以亦沒有失望。至於有些影評扮高深解構電影的創造論理,我只可以說編劇連最基本劇情不要犯駁都寫不好,就不要指望他有能力去表述更深層次的意思。作為一套送爆谷的娛樂驚嚇片,不計非常沉悶前半部的話,後半部不過不失,不妨一看。不知道是否我看得多異形變有點麻木了,我嫌這套電影不夠恐怖嘔心,希望下集可以拍得更驚嚇吧。

反斗車王3

不經不覺《反斗車王》已經有十年歷史,第二集白痴Mater做主角令故事超爛,以為Pixar把這系列玩死了。想不到第三集找回初心,再以賽車場比喻人生,為這系列劃上一個完滿句號。戲中時間與現實一樣,十年過去主角McQueen從第一集的新晉小子,漸漸成熟為車壇老將,勝出四次Piston Cup大賽,比師傳Doc Hudson還要多一次。可惜長江後浪推前浪,面對新世代跑車的挑戰,不論是引擎馬力,車身風阻,最高時速等,上一代的車款在比賽中顯得力不從心。與McQueen同期的車手,大部份都退休了,讓出位置給跑得更快的新人。昔日的車神面臨中年危機,在退與不退之間要作出選擇。可是他對跑道亦仍留戀,不甘心就此退下來,希望再闖高峰,保持王者地位。

下文包含劇透,不過電影玩具的車身拉花,早己經完全劇透了,所以在此我透不透也沒多大關係。

第三集與第一集的格局很相似,開場第一場比賽主角落敗(還要炒車大難不死),中段是很王道的練功加尋找自我的旅程,最後結尾的那一場比賽反敗為勝。第一集的「壞人」是出矛招的綠色鬍鬚車,這集的「壞人」則是目中無人的新晉車手Storm,戲中沒有說他們二人是師徒關係,不過二人同樣喜歡撞人,可能有點淵源。McQueen的贊助商Rusteze被賽車迷億萬富豪收購了,他出手闊卓興建高科賽車技訓練中心,決心建立一隊最頂尖的車隊。黃色跑車Cruz原來是McQueen的訓練員,亦是這齣電影的女主角。不過觀眾不用擔心Sally的正印地位,她和McQueen只限於師徒關係。仍舊與第一集一樣,中段笑聲不絕,McQueen老人家不適應高科技訓練模式,轉移陣地沙灘到特訓,然後McQueen和Cruz誤打誤撞參加了Demolition Derby(即賽車MMA混戰),特別是McQueen智勝怪獸校巴那段,阿仔笑到起身拍手。

第一集故事的轉折點是McQueen發現Doc Hudson的真正身份,而這集的轉折點是Cruz講出她想當車手的夢想,身為女生不被接納當不成車手,只好退而求其次當訓練員。電影初段一直有舖排Cruz的賽車天份,從她輕輕鬆鬆在模疑器上跑出佳績,沙灘特訓剛學慬跑沙地便能追貼McQueen,在Demolition Derby大混戰中存活下來並奪得冠軍,加上預告中的劇透,這轉變完全不意外。第一集McQueen從Sally身上學懂慢下來的道理,這一集則從老前輩身上,學懂薪火相傳的道理。當年Doc當他的師傳,找到跑道的第二個意義,現今McQueen把當年從Doc身上學到的,回饋給Cruz。結尾那場賽車的高潮,並不是McQueen反敗為勝,而是他退下來成全Cruz,給她一個當賽車手的機會。至於Cruz使出Doc的「絕招」反擊Storm,大慨已是觀眾意料之內的套路。第三集與第一集一樣,雖然McQueen沒有贏得比賽,但他贏得比獎盃更加重要的東西。

《反斗車王》一向被批評為在眾多Pixar作品中缺乏深度,今次大結局(車王都退休了,應該不會再拍續集吧)竟然有驚喜。McQueen的中年危機小朋友肯定看不明白,但陪太子睇戲的家長相信會有所共嗚。戲中的道理拍得淺白,年輕時總有無窮無盡的夢想,認為自已能有一番作為。可是隨年紀增長,不能夠永遠拼死硬闖向前衝,轉而憑經驗智取補救力量上的不足,勉強應付一眾新人的挑戰。然而花無百日紅,沙場上不許見白頭,總有一天要退下來。高峰過後退下來,如何適應轉換跑道,大慨就是所謂的中年危機。退可以退得很蕭灑,像McQueen一樣提攜後輩,退而不休贏得尊敬。亦可以不情不願留戀高位,繼續當個老海鮮指手橫腳,阻住個地球轉。但時間永遠站在新世代那邊,最後在鬥爭敗陣被迫退下來,恐怕連身為前輩的尊嚴也輸掉。

Frame Arms Girls 骨裝機娘

《骨裝機娘》是一部不折不扣的玩具廣告,賣的是壽屋的Frame Arms Girls模型系列。本家的Frame Arms是機械人模型,主打通用骨架配各種武器。Frame Arms Girl則是保留武器,把機械人的骨架改為少女。其實機械人少女(統稱機娘)的商品不少,除了壽屋外,還有Konami的武裝神姬和笨大的AGP高達少女。高達少女以高達為背景定位清楚,其他沒有動畫的機娘,只有人設,面目蒙糊,我也分不清楚誰打誰。沒有原作故事支撐的玩具角色,感覺上面目很難投入,說服讓玩家購買很脫力,大慨因此壽屋才要拍動畫谷銷量。

這部動畫是低成本製作,機娘的CG戰鬥畫面完全不合格,動作生硬打鬥設計馬虎。不知裏就先亂打一輪,然後忽然一招大絕KO對手。不過戰鬥根本不是重點,這套作品主力玩日常搞笑,女主角和機娘們大開百合。每集是獨立短篇故事,除了女主角外,就只有另一個人類角色模型宅,她的作用是介紹砌模型的小知識。在一個廣告動畫中再置入廣告,到底是什麼玩法?不過廣告倒很成功,我記得那把鬼魂上身的壽屋神剪。

要賣玩具機娘自然越出越多,最後有八隻機娘寄居於女主角家。沒有主線就沒有包伏,單完劇情可以玩得很癲,什麼異想天開的點子也可以拍出來。雖然有點白痴無聊,但勝在好好笑,這套應該算是治癒系吧。機娘玩相撲,叉電君的觀音兵傻樣,機娘玩公仔屋佈置自已間房,把機械吸塵機變為座駕,外出幫主人購物大作戰,主角發夢機娘變成真人同學。最好笑那話是忍者機娘認為正宗著和服唔可以著底底,於是潛入剪了主人條底底,保衛底底大作戰。賣萌百合番一定有浸溫泉賣肉的指定動作,不過機娘不是模型嗎,為什麼她們可以除衫浸溫泉?

沒有期望就不會失望,每週輕輕鬆鬆看一集,沒有追看故事的壓力,甚至覺得隨時砍番也不可惜,不過就是一集接一集的看到結局。多得動畫化,Frame Arms Girls比本家Frame Arms更有人氣,有點本末倒置的感覺。不知道壽屋會不會添食,索性出本家Frame Arm的動畫,如果成事就太好了。

Formal Verification – Erik Seligman, Tom Schubert

這篇不是書評,這本書亦不是一般自學程式設計的電腦書,是一本涉及非常專門的知識,只有設計晶片才會用得上的技術課本。非行內人完全看不明白,這篇只是我學習formal verification(形式化驗證)的心得和筆記,所以我亦不期望有什麼讀者。

什麼是Formal Verification?首先要講什麼是dynamic verification,設計晶片不同寫程式,寫程式有bug很簡單,除錯出patch沒有什麼大不了。晶片有bug就很大件事,因為要更正問題,就要重新tape-out多一次,去做一個全新的mask。可以想像製造晶片好印黑膠碟,先要整有一張母碟,然後才可以覆印,mask就是silicon的母碟。傳統上測式晶片設件主力用simulation(即dynamic verification),要花很多人力物力寫個testbench出來,然後模疑晶片所有的input同output。這是一個非常嚴格的工序,因為一個bug也不可以走漏。晶片出了街之後,fix一個bug的成本是幾百萬美元。寫testbench同寫普通software沒有太大分別,只不過測試硬件比測試軟件嚴格很多。Formal Verification則是用另一個方法去測試硬件,不用寫code,寫formal specification,再用數學邏輯理論,去證明硬件的設件必定等於那個specification。完全不同的思考方法,完全不同的用途。Formal Verification可以測試出simulation找不出來的bug,始終simulation並不是exhaustive,不過formal有很多限制,設計不能太大不能太深,始終formal proof係一個NP-complete problem。

多年來formal一直只是學術研究,真正的商業應用,大約五六年前才開始。早期的formal tool非常難用,常常被戲說要博士才懂用,很多designer聽見便敬而遠之。直至JasperGold的推出,formal才開始普及化,這些年來JasperGold手執牛耳,一枝獨秀差不多等同於formal的代名詞。早兩年我也嘗試過學formal,不過當年JasperGold的license太貴,我們細公司買不起,只好用了一個很差很難用的IFV,結果學師未成不了了之。去年我公司被一個大公司收購了,economy of scale讓我們有多好多tools用,今個project終於有機會用到JasperGold,同IFV相比簡直是天堂和地獄,「工欲善其善,必先利其器」,其實formal一點也不難,我花了兩星期便滿師,可以學懂簡單的formal specify,去proof我個design不會有dead lock。如果要用simulation作同樣測試,因為太多corner cases,是一件非常痛苦的差事。現在用formal去做,幾行code寫完,是一件很好玩的玩意。

我一直都有follow開formal的paper和tutorial,雖然沒有實戰經驗但formal理論大至明白,用新tool不過是學syntax,很快上手。我公司的formal expert介紹我看這本《Formal Verification》課本,這本書是三位Intel工程師編寫的,由淺入深講解很有系統地如何應用formal verification,真正的hard-core技術含量不多(技術東西可以自已看document),反而更像是過來人分享心得和經驗。這本書九成是老生常談,平時睇tutorial睇paper都學過聽過,不過餘下的一成非常有用,讓我茅塞頓開,很多看已paper不明白人家為什麼一定要這樣做的地方,經他一解釋完全明白,一理通,百理明。這本書可以說是我formal的啟蒙老師,任何一個初學formal者必定要看。市面上formal的textbook一隻手數得完,因為formal是太專門的技術,譎想想學就要交很貴學費請consultant去教,不過我認為這本書比consultant教得更好,因為作者有真正的實戰經歷,不似consultant般大多紙上談兵。

以下是我認為書中有用的formal「心法」:

  1. cover和assert是同一塊鏡子的兩面。同一個property,cover就是not左個property的assert的counter example。assert就係not左個cover既unreachable proof
  2. Formal engine係一個breath-first咁去行所有的state space。assume同assert就係cut細個state space,cut走左illegal state,如果行到去specification果個state,咪就proof度囉。
  3. 一開波不要立即寫full proof,先由cover開始玩。唔用assume,剩係寫你想睇乜output,睇下formal engine可不可以back trace你想要的input,然後再慢慢fine-tune那些assume
  4. 用cover整好晒assume,就可以上去bug hunting,專心搵assert的counter example,最後才整full proof。用之前兩個steps的assume
  5. 唔好load太多code,太多assert同cover,要divide and conquer。有些tricks可以用,如cutpoint,abstraction,free variable等等