# dataset-for-mcVer-timed

**Repository Path**: fmpa/dataset-for-mcVer-timed

## Basic Information

- **Project Name**: dataset-for-mcVer-timed
- **Description**: dataset for the pupal version of mcVer
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 1
- **Forks**: 1
- **Created**: 2021-10-25
- **Last Updated**: 2023-12-25

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# dataset-for-mcVer-timed

## 介绍
该文件夹中是利用UPPAAL进行验证的合约实例。其中每个文件夹中包括了（.sol）结尾的合约文件，（.xml）结尾的模型文件，（.q）结尾的性质文件，工具验证后的结果文件为（.txt）结尾

## 模式展示

- ### 模式一：单一时间期限

    - 模式描述：合约设置了一个期限(aDL)，承诺在此期限内完成某些任务，期限外拒绝服务。
    - 表现形式：

        ![](./img/1.gif)

        在函数A中,通过获取当前区块上的时间戳后设置合约期限aDL。当函数B被执行,获取时间戳来判断此刻是否超过期限。

    - 这种模式的合约一般需要满足以下承诺:
        1.	在规定期限内(block.timestamp<=aDL),合约必须完成承诺的任务;
        2.	在期限外(block.timestamp>aDL),合约拒绝某些服务;
        特别注意边界情况(block.timestamp=aDL),合约应执行所承诺的任务;

    - 实例：SimpleAuction

- ### 模式二:分段时间期限

    - 模型描述:合约中设置了分段期限，不同期限段内承诺的任务不同。

    - 表现形式：
    
        ![](./img/2.gif)

        在函数A中设置了两个期限aDL和aDL’,其中aDL’>aDL。在函数B执行时，判断当前时间处于第一期限内、第一期限外但第二期限内、或第二期限外,不同时间段内执行任务不同。

    - 这种模式的合约一般需要满足以下承诺:
        1. 在期限aDL范围内,合约必须完成承诺的任务A;
        2. 在期限aDL外但aDL’范围内,合约必须完成承诺的任务B;
        3. 超过期限aDL’,合约拒绝服务;
        特别注意在时间边界上合约应该只能有一个任务成功;

    - 实例：TrackSystem

- ### 模式三:时间期限延长

    - 模式描述:为吸引更多参与者,在接近原定合约期限时延长期限。

    - 表现形式:
        
        ![](./img/3.gif)

        在函数A中设置原始期限aDL.在函数B执行时,判断当时的时间戳是否接近原期限值(相差t单位时间),如果接近,要对合约期限aDL进行延长,延长一个时间段(extime).函数B的每次执行都有可能做此延长.

    - 在这种模式的合约一般需要满足以下承诺:
        1. 合约可终止;
        2. 合约终止后能完成规定任务;

    - 实例：Auction_extend

- ### 模式四:多重时间期限

    - 模式描述:合约对不同用户设置不同期限。

    - 表现形式：

        ![](./img/4.gif)

        在函数A中对不同用户设置时间期限aDL[msg.sender]。函数B被执行时，判断是否满足当前用户的时间期限。

    - 这种模式的合约一般需要满足以下承诺：
        1. 用户k在自己的期限 (aDL[k]) 内请求服务,合约必须完成承诺的任务;
        2. 对于用户k在自己的期限 (aDL[k]) 外的请求,合约拒绝服务;
    
    - 实例：TimeLock

- ### 模式五:相对时间期限

    - 模式描述:以合约期限内的某一时刻为起点，设置一个相对期限，承诺在此相对期限内完成某任务。

    - 表现形式：

        ![](./img/5.gif)

        在函数A中设置原始期限aDL.在函数B执行时,判断当时的时间戳是否在合约期限内,如果在,设置一个从当前时刻开始的相对期限aDL’.在函数C执行时根据当前时间是否在相对期限aDL’内进行相应操作.

    - 这种模式的合约一般需要满足以下承诺:
        1. 如果在aDL期限内完成任务B,那么一定可以在其后的aDL’内完成任务C;
        2. 如果超过aDL还没完成B,那么合约拒绝服务;

    - 实例：Shopping

## 实例研究
- ### 航班延误
    - 合约描述：乘客购买机票之后的30分钟内需要购买保险,对应的保险公司会预存相应的赔偿金；如果保险公司没有按时预存赔偿金,系统就直接将保费退还给用户;如果保险公司预存了赔偿金,乘客乘坐的航班没有延误,保险公司可以获得保费并撤回自己预存的赔偿金;如果航班延误,保险公司可以获得保费,但将保险公司预存的赔偿金赔偿给乘机人。
    - 实例：FlightDelay
    
- ### 购物
    - 合约描述：购物合约中规定了优享时间、实惠购物时间、发货时间限制和商品下架时间,购物者优享时间之前下单可享受5折优惠,超过优享时间但早于实惠购物时间下单可享受8折优惠,之后在商品下架前按原价购买;当购物者下单后,商家应该在发货时间限制内发货,如果没有按时发货,购物者有权申请退款,但是在下单3天后才可以申请退款需要。
    - 实例：Shopping