从以下两个项目中选做其一：
一、图书索引处理（可独立或合作完成，同组合作者不得超过2人）：
本项目基于真实的索引处理工具makeindex[1,2]、xindy[3]等，我们将使用Python语言实现这些工具功能的一个子集。在项目中，我们将熟悉文件处理类程序的组织和编写，可能会涉及表（数组）、集合、字典、栈、正则表达式等数据结构及排序等算法的灵活使用。
篇幅较长的科技图书经常会有关键词索引。索引的格式是：将关键词按字母顺序分类排序，在关键词的后面标记出关键字所在的页码。本项目说明的末尾就有一个简单的名词索引。在现代图书出版中，名词索引通常是使用如下方式生成的：(1) 作者在撰写图书时，在正文中标记出需要做索引的词汇。(2) 排版软件处理图书正文时，将标记出的词汇与词汇所在的页码从正文中提取出来，成为单独的索引文件。(3) 索引处理工具对提取出的索引文件按字母分类、排序，并且将相同的条目合并起来。本项目的任务是要编写一个索引处理工具，完成上面的第3个步骤。
1. 索引的输入
不同的排版软件可能生成不同格式的索引文件，为方便计，我们采用比较简单的一种格式，它也是计算机科学的经典著作《The Art of Computer Programming》的索引文件样式。每个索引文件许多行构成，每行是一个索引条目。一个索引条目分为两个部分，索引词和词条所在的页码。索引词与页码之间用一个空格与感叹号分隔开。简单的条目如：
Fibonacci sequence !13
它表示索引词是“Fibonacci sequence”（斐波那契数列），出现在全书的第13页。
索引词可能会在多处出现，因此同一个索引词可能会有多个页码；同一页的索引词也可能被多次标记。因此，有可能出现这样的索引:
Fibonacci sequence !13
Fibonacci sequence !13
golden ratio !13
Fibonacci sequence !27
有时，作者在书中的一整段内容都是关于一个名词的，因而会为这个名词标记一个页码区间。可以使用如下两种方式：
(1) 在索引词的后面加上若干个加号，表示这个词条的会向后延续加号这么多页。例如：
memory+ !4
assertions+++ !15
表示“memory”这个词条出现在第4页到第5页，而“assertions”词条会出现在第15-18页。
(2) 在索引词的后面与前面加上两个减号，分别表示词条的开始与结束的位置。例如：
arithmetic operators of MIX-- !131
--arithmetic operators of MIX !133
表示词条“arithmetic operators of MIX”从131页延续到133页。
索引条目的页码都是阿拉伯数字。但是，并不保证索引输入文件中的索引条目是按页码顺序排列的。
如果对项目进行扩充，可以在上述描述的基础上，支持更多或更复杂的输入格式。
2. 索引的排序
索引处理程序的主要工作就是对索引进行排序。
2.1 索引词排序与分类
大体上，需要将索引词逐字符按字典序进行从小到大排序。但有如下特殊规则：
(1) 如果字符串只包含阿拉伯数字（自然数），则数字大小比较。例如，“9”应该排在“10”之前，尽管按字符串序符号“1”在符号“9”之前。
(2) 以符号开头的字符串总是先于排在以数字开头的串，而这又先于纯数字的排序项和以字母开头的串。
(3) 在比较两个字符串时，索引处理程序应该首先忽略字母大小写进行比较，如果此时结果相等，再按区分大小写进行比较，将大写字母排在小写字母之前。
排序后的索引将进行分组。共分为28个组：完全由阿拉伯数字的组成的条目（自然数）分入“Numbers”组，以符号开头的条目（包括数字开头但不是纯数字的条目）分为“Symbols”组，其他条目按首字母分为26个组。不需要考虑希腊字母、汉字等无关的内容。
2.2 页码排序与合并
同一索引词的输入条目将会合并为一项，该项可能会有多个页码。
对合并后的每个索引项，需要对页码从小到大排序，去除重复的页码。例如，输入的索引项为
Fibonacci sequence !13
Fibonacci sequence !27
golden ratio !13
Fibonacci sequence !13
输出应只包含两项，形如：
Fibonacci sequence, 13, 27
golden ratio, 13
需要注意页码区间的合并，例如：
item-- !1
item !5
item++ !7
--item !10
item !10
应该直接合并为
item 1-10
并且注意相邻的页码区间也要合并为同一项，如
item-- !1
--item !3
item-- !3
--item !5
item !6
应合并为
item 1-6
可以对项目进行扩充，在上述描述的基础上，支持更多或更复杂的排序规则。
3. 索引结果输出
索引处理程序在对读入的索引项排序整理后，需要将结果输出。
结果按28个分组分别进行输出，即按数字组、符号组、26个字母组输出，输出时跳过没有条目的分组。输出每个分组时，先输出分组名称（Symbols, Numbers, A, B, . . . , Z），空一行后开始输出这一分组的条目。分组之间空两行。
对于每个条目，分别输出词条本身，与词条所在的页码。词条与页码之间、页码与页码之间用一个逗号和一个空格分隔。页码经过排序和合并，3页或3页以上连续的页码区间在起迄页码中间用两个减号分开。词条最后输出一个西文句号。
下面是一个输出的例子：
可以对项目进行扩充，在上述描述的基础上，支持更多或更复杂的输出格式。
4. 可能的扩展功能
索引程序可以有多方面的扩展，例如支持不同的输入格式，支持更复杂的结构等。
(1) 考虑如何在输入中进行转义处理。例如，当使用感叹号、加号、减号作为特殊字符时，如何处理索引条目中的感叹号、加号和减号。
(2) 考虑如何使输入输出的条目的格式变成可配置的，如让程序读入一个配置文件，在配置文件里面决定输入的特殊符号、输出的模板等。
(3) 考虑支持更复杂的结构，例如多级条目，一个条目下又可以有多个子条目。又如多级数字（可以表示章节编号而不只是页码）。
(4) 考虑支持更复杂的排序与分组规则。可以允许在条目中指定输出的文字与用来排序的文字不同，如希腊字母 可以按alpha来排序。设计对应的输入语法，输出的格式。
(5) 其他你认为有用的扩展功能。
其他可能的扩展功能可以看makeindex[1,2]、xindy[3]等工具。
5. 项目要求
完成下面的项目要求，将项目索引处理程序、测试用例文件、测试结果文件、项目报告一起打包，提交作业。
5.1 索引处理程序
编写索引处理程序，完成前述的基本功能，并在第4节中至少选择两种扩展功能加以实现。
程序由若干个模块组成，其中包含一个Python脚本indexing.py。脚本用法如下：
python indexing.py?输入文件名? ?输出文件名?
如果有扩展功能，可以在?输入文件名?之前增加其他的命令行参数。
5.2 索引表生成
自己设计一些用于测试的索引条目，生成索引表，验证程序的功能。你编写的测试示例应该能验证：
（1）条目分组与排序的规则。
（2）页码排序与合并的规则。
（3）你设计的各种扩展功能。
随项目附有《The Art of Computer Programming》原书第一章的真实的索引数据文件taocp-1.idx，请使用你编写的程序，根据此数据文件，完成索引表的生成。
5.3 项目报告
根据项目完成的情况，编写项目报告。报告内容包括：
（1）对问题的简要描述与分析。应具体说明在你的项目中决定提供哪些功能，提供了哪些扩充。对于本项目说明没有详细说明的扩充功能，应详细分析其效果和用法。
（2）程序模块划分与具体数据结构的设计。除了说明设计的结果，也要说明设计的原则与取舍过程。
（3）程序实现中的关键问题和技术分析。
（4）概述系统功能完成情况。分析测试用例的输出效果，加以适当说明。
（5）程序重要算法的时间复杂性分析，及程序过程的空间复杂度分析。除了进行数学化的渐近复杂度分析，也可以给出实际运行的时间数据，说明程序的实际有效性。
（6）进行系统完成后的回顾和分析。说明程序的优点、缺点，可能的改进问题，在编写项目中曾经遇到的困难与解决方案，走过的弯路等。
项目报告使用PDF格式提交。报告写清楚标题、项目参与人的姓名学号。报告应按内容合理划分章节，注意算法、公式和代码的格式，使内容清楚，易于阅读。
参考材料
[1]Leslie Lamport.MakeIndex: An Index Processor For LATEX, February 1987. URLhttp://mirror.bjtu.edu.cn/CTAN/indexing/makeindex/doc/makeindex.pdf.
[2]Pehong Chen and Michael A. Harrison. Index preparation and processing.Software—Practice andExperience, 19(9):897-915, September 1988. ISSN 0038-0644. URLhttp://mirror.bjtu.edu.cn/CTAN/indexing/makeindex/paper/ind.pdf.
[3]Roger Kehr.xindy Manual, January, 2004. URLhttp://xindy.sourceforge.net/doc/manual.html
这里有一个文件，是一部著名计算机专著的一部分索引，作为本项目的参考数据文件。
二、LTL/CTL模型检验（可独立或合作完成，同组合作者不得超过3人）：
有限状态迁移系统（Finite Labelled Transition System) 是形式化验证中常用的模型之一。一个有限状态迁移系统包含有限个状态（State）和一系列的迁移（Transition），每个迁移包括起始状态，后继状态和一个动作，当系统处于起始状态时，可以执行该动作并跳转到其后继状态。一个简单有限状态迁移系统的例子（Coffee Machine）定义如下所示：
idle paid
idle
coin idle paid
coffee paid idle
第一行给出所有状态的名称（名称只能包含大小写英文字母和数字，用空格隔开）。在这个例子中，咖啡机共有两个状态，分别是待机（idle）以及已付款（paid）。第二行给出系统的初始状态，在这个例子中为idle。之后每一行描述一个迁移（三个由空格分开的字符串，分别是动作名称，起始状态和后继状态）。其中起始状态和后继状态必须是第一行中出现过的。
一个有限状态迁移系统的运行过程如下：
最开始，系统处于其初始状态
如果系统的当前状态上存在一个迁移，那么就执行这个迁移并跳转到它的后继状态
如果存在多个迁移，系统会随机选择一个执行
将系统执行过程中的状态序列记录下来，我们称为它的一个路径（Path）。例如，例子中系统的路径可以是如下的无限序列：
idle, paid, idle, paid, ...
显然，一般情况下，一个有限状态迁移系统所对应的路径不是唯一的，而是一个集合。
时序逻辑用于描述系统满足的时序性质，常用的时序逻辑包括线性时序逻辑、计算树逻辑等。例如线性时序逻辑（Linear Temporal Logic）可以描述一个系统在线性时间上的变化所要满足的条件。一个线性时序逻辑公式L的定义如下所示：
L：：= True | a | L1 and L2 | not L | X L （next）| L1 U L2 （until）
具体含义见[1]，[2]。
假设我们有一个线性时序逻辑公式（X paid），那么我们可以看出上述的系统是满足这个公式的。因为它唯一的一条路径上从初始状态开始，下一个状态就是paid（这很显然！因为总共只有两个状态……）
如果给定一个有限状态迁移系统TS和一个线性时序逻辑公式L。当且仅当TS所有可能的路径均满足L时，我们说TS满足L。
基本要求：
设计并实现一个LTL/CTL的模型检查工具，使得对给定的状态迁移系统TS和LTL/CTL公式L，可以判断TS是否满足L，若满足，返回True，若不满足，返回False并给出TS中一条不满足L的路径作为反例（CTL中对于存在量词公式成立时返回一条满足公式的路径作为witness）。并对所给出的实现进行性能分析。
示例输入文件格式：
第一行为n个用空格分开的字符串，描述状态迁移系统的每个状态名称。第二行为一个字符串，描述状态迁移系统的初始状态。之后的若干行为状态迁移系统的边，每行由三个字符串组成，分别是：动作，起始状态，目标状态。中间用空格隔开之后空一行。然后每一行是一条要检查的时序逻辑公式。为简化问题，我们假设任何运算都由括号括起，从而不存在优先级的问题。到文件结束为止。
示例输出文件格式：
m行（m为公式的条数），每行为True，或者False加上一个状态序列作为反例，表明该模型满足公式或者不满足且给出反例。
选作：
1. 在LTL/CTL公式中可使用其他扩充运算符，如eventually、always、weak until等。
2. 设计并实现其他时序逻辑（如CTL*、TCTL、PCTL等）的模型检验算法。
报告要求参见第一题。
注意：
1. 感兴趣的同学可以考虑选作内容，不做这部分的内容不会导致本次报告成绩降低。
2. 数据结构的设计和算法的效率是需要重点考虑的问题，不需要把太多的时间花在图形界面上。做了图形界面并不是加分项。
3. 可自己定义输入输出文件格式，但需在报告中说明。
参考文献（[1]、[2]为院图馆藏）：
[1] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.
[2] Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled. Model Checking, The MIT Press, 1999.
[3] Some widely used model checker: PRISM, UPPAAL, mCRL2
|
