4 months ago

年轻好啊

敏捷

每个人都该年轻

 
4 months ago

SL may refer to:

特殊线性群 (Special Linear Group)

Snowonion LEE

我.

Save / Load

部分游戏的一类玩法.

Symmetric Logspace 计算复杂度

TODO

Etc.

https://en.wikipedia.org/wiki/SL

 
7 months ago

Zero score and seven years ago,

2009 年 1 月,高一寒假,我和爸妈回湖南。

在那趟卧铺上,我用我妈的摩托罗拉翻盖机与小伙伴发短信保持通讯。
用一个能看 .txt 听 .mp3 的山寨学习机来摆脱无聊(努力节省电量;到了舅舅家赶紧给七号电池充电)。
在老家,拍农田和县城建筑,更新百度空间相册,BGM 梁祝小提琴协奏曲。
回忆初中,并认为毕业半年后是回忆强度的巅峰:太近则还没开始怀念,太远则细节都忘掉了。
刘一哲 《为年轻人申辩》并不完整的版本
(作者博客原文地址(5 被和谐了?):1 2 3 4 6 7
刘一哲主编的《说事》杂志教给我,要讲道理。杂志的一部分的 txt/doc和杂志的全集的 pdf
包里有《龙门专题:极限 导数 微积分》
拍摄南县一中「游泳池」

Zero score and four and a half years ago,

2011 年 8 月,高考暑假,我和爸妈回湖南。

在那趟卧铺上,用我爸充话费送的然后给我的联想 TD80 与小伙伴发短信保持通讯。
与一个弟弟玩一个能自动寻路的网游。(好吧,也许是 2009 年的场景。)
与另一个弟弟和一个姐姐去游乐场玩,过山车、摩天轮及其他。
包里有张筑生《数学分析新讲》
又去拍摄南县一中「游泳池」

Zero score and zero year ago,

2016 年 2 月 7 日,在久违的超早入睡(九点)之后醒来,以为是三点其实才零点。

在这趟卧铺上,用少女(阿里嘎多!)拿她和我做外包的工程款中归她的那部分的一部分买了送我的 iPhone 6,在 QQ、微信、Twitter、微博、Ingress、邮件、短信,与很多人——却在能触及的人里面只占极少的比例——保持通讯。
也没有什么「保持通讯」。「中断通讯」才是新闻。
列车沿京广线向南;地图定位在驻马店南边;网路在 3G / 4G 之间切换,偶尔 E / GPRS.
包里有汪芳庭《数理逻辑》(感谢 Q 同学当时给我推荐的李未の书- -),柯谁谁谁谁《代数学引论》(感谢 GL 同学!),《计算机程序的构造和解释》(直播做习题的 Github 仓库)(这个 SICP…… 西方记者 张同学 大一就学了吧……)
我已经是数盲了…… 给自己扫扫盲吧
谜之自信
先承认不会,才能够去学…… 勒夏特列原理 / 楞次定律
而上次去游乐场那个弟弟,高二开学那次物竞分数能进省队,年后大概初三要去集训……
(Fucking admire!(参考翻译:钦羡
也许我会再去拍南县一中「游泳池」……

生活,参数,默认值。

alias grep = 'grep --ignore-case --colour'
clang++ xxx.cpp = clang -std=c++11 xxx.cpp
Ubuntu 1x.yz = Linux 内核 + apt 包管理器 + Unity 桌面(仅作文使用!不保证技术细节准确……)
基本上没有什么不能替换的。
基本上没有什么不能尝试的。(嘛 太鸡汤了。在解空间里取一个点,这个点是「可尝试的」的概率目测是 0)
宇宙很大,生活很大。
不太严格地讲:
现实世界是所有「可能世界」中的一种。可能世界是逻辑自洽的「世界」。一个世界是一组命题的集合,含义是“在这个世界中,这些命题为真”。
(感谢 ZYQ邵菊苣!这半年来。)
「发现更大的世界」是吧。

这几个月,有时我脑中会回响:

「窝们到底重不重要
窝们是不是很渺小」

你看你也回响)

怎么讲,当我慢慢长大,走近这个世界,我先觉得自己变得重要,然后觉得自己不那么重要,如下图所示:

(嘻嘻,强行解释





台风

一条银鱼在黑暗里翻了个身
几乎没有声音
刀锋一样的银线割破睡着的人的喉咙

茶汤溅在褐色的地板上
你起身,披一条床单
走到阳台上
你看见:星辰混在一趟绿皮火车里远去

作者:大喘气
出处:这里那里

2016-02-07 02:34:26, Z77(非绿皮),武昌站

 
7 months ago

有点简略,如果你已经知道时间自动机和 UPPAAL 就完全可以看懂…… 哎我尽量 self-contained,目标是让所有读者至少能看懂九成……

(如果想了解时间自动机和 UPPAAL,可以看一看 [译]时间自动机:语义,算法和工具,不看也行 )

1

昨天晚上 ZH 同学在群里发了张图:


走迷宫,但是经过的圆点必须红蓝交替。

2

不一会,LJ 同学给出了一个解:


WX 等同学表示 LJ 真会玩。
HK 同学给出了另一个解,但我没看懂文字描述?

3

早上起来,发现昨晚 JSK 同学一点多的时候说了一句:

这不是形式化验证问题吗?

我有点兴奋,于是想到以前用过的模型检测工具 UPPAAL 来解一下。UPPAAL 有 GUI,有模拟器,有属性验证器,很适合这道题。

4

于是就去建模了。

考虑了时间自动机的 Location(i.e. 圆圈)应该表示题目中的”十字路口“还是”圆点“。结论是十字路口。

考虑了”被没有圆点的道路连接的十字路口 是否应该合并成一个 Location“的问题。经过失败的尝试:


结论是不应该合并。

在添加任何约束条件之前,模型是这样的:

考虑了“用 Channel + Synchronization 还是 变量 + Guard 来描述红蓝交替这个约束”的问题。结论是 Channel + Synchronization。因为在自动机进程图里有一大堆 Edge;在每个 Edge 上标记 r? 比 color==1 要简短和清晰……

于是,加了一个”乌鸦“自动机,用来发出信号;让原自动机接收信号。建模完的样子:

经过几次用模拟器 Debug,查了一些“忘写 Edge 的 Sync”的错误;否定了把乌鸦自动机的 Location 设为 Committed / Urgent 的想法;
然后用验证器验证这个属性:

E<> rbp.T

即:从系统初始状态出发,存在(E)一条执行路径,使得自动机 rbq 可以(<>)到达 Location T。
(在不涉及 时钟/变量 的时候,时间自动机系统的状态就是所有自动机的 Location 组成的向量/元组。)

好的,这俨然是个图论问题……(有什么模型检测问题不是图论问题吗(有什么问题不能转(juǎn)化成图论问题吗))

验证通过!然后设置 Diagnostic Trace 策略为 Shortest,再验证一次,输出执行路径:


这就是 LJ 同学的解嘛!好棒好棒的!

大致就是这样。

Appendix

  1. 建模时烦人的事:加 Edge;拖动 Edge 的控制点到美观的位置;给 Edge 加 sync;拖动 sync 文字(r? 和 b?)到美观的位置;给 Location 取名字……

    必须有一门迷宫建模的 DSL 了!
    
  2. 录屏生成 GIF 的软体是 LICEcap,有 Windows 和 OS X 版,好使。从 小众软件这里看到的。

  3. (iOS 和 OS X 的)微信里发 GIF 动不起来?Bad。

  4. 群里聊这个题的时候我画了个图,解释 UPPAAL 在世界中的位置(啊,窝好喜欢“我们在世界中的位置”这个词……):


    对不对呢?感觉有必要跟贺师和罗师求教一下……

  5. UPPAAL 下载:http://www.it.uu.se/research/group/darts/uppaal/download.shtml
    下载需要填个表格…… 不用太在意。
    我用的是 OS X 4.0.13。刚才又下了一下,不能用…… Windows 4.0.14 版却能用……
    模型文件:http://7tsy1b.com1.z0.glb.clouddn.com/program%2Fuppaal_red_blue_puzzle.xml
    属性文件:http://7tsy1b.com1.z0.glb.clouddn.com/program%2Fuppaal_red_blue_puzzle.q

 
8 months ago

軟體工程師 = 軟體の工程師