This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Model Checking

Given a system model, we try to check whether it meets its specification automatically and exhaustively.
To describe/represent the system and specification, we use Automata over infinite objects.

Verification Problem

The verification problem can be solved by:

Constructing the intersection of system, with an automaton for the negation of the specification,
then checking whether the language of the resulting automaton is empty.

$\textbf{Example 1.1. } \text{Consider the concurrent program }\small{\text{TURN}}:$
$$\text{local $t$: boolean where initially $t$ = $false$}\newline
P_0::\left[ \begin{array}{l}\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
\ell_0: \text{await }\neg t; \newline
\ell_1: \text{critical;} \newline
\ell_2: t := true; \newline
\end{array} \right]\end{array} \right]
\mid\mid P_1::\left[ \begin{array}{l}
\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
m_0: \text{await } t; \newline
m_1: \text{critical;} \newline
m_2: t := false; \newline
\end{array} \right]\end{array} \right]$$

The example above is a simple solution to the mutual exclusion problem:
it ensures that at any given point of time, at most one process is in the critical region.

From Program to automaton

To represent the above program using automaton, we need to define an alphabet $\Sigma$.

Question

Table name: Weather

Column Name	Type
id	int
recordDate	date
temperature	int

There are no different rows with the same recordDate.
This table contains information about the temperature on a certain day.

Write a solution to find all dates' id with higher temperatures compared to its previous dates (yesterday).
Return the result table in any order.

Explaination

Here, we need to learn how to handle the datatype date.
To modify the date, we can use INTERVAL keyword, or DATEADD() function.

INTERVAL <value> <unit>

Interval is a special datatype, that can interact with time and date.

Interval unit includes
microsecond, millisecond, second, minute, hour, day, week, month, year, decade, century, millennium

Question

Table name: Visits

Column Name	Type
visit_id	int
customer_id	int

This table contains information about the customers who visited the mall.

Table name: Transactions

Column Name	Type
transaction_id	int
visit_id	int
amount	int

This table contains information about the transactions made during the visit_id.

Write a solution to find the IDs of the users who visited without making any transactions, and
the number of times they made these types of visits.
Return the result table sorted in any order.

Explaination

This is another typical JOIN query question.
The tricky part is the column we join on doesn’t necessarily be selected.

Question

Table name: Sales

Column Name	Type
sale_id	int
product_id	int
year	int
quantity	int
price	int

Each row of this table shows a sale on the product product_id in a certain year.
Note that the price is per unit.

Table name: Product

Column Name	Type
product_id	int
product_name	varchar

Each row of this table indicates the product name of each product.

Write a solution to report the product_name, year, and price for each sale_id in the Sales table.

Explaination

This question is a basic usage of JOIN query.

Question

Table name: ``

Column Name	Type
user_id	int
name	varchar
mail	varchar

This table contains information of the users signed up in a website. Some e-mails are invalid.

A valid e-mail has a prefix name and a domain.

domain: @leetcode.com.
prefix name is a string that may contain:

• letters (upper or lower case)
• digits
• underscore _
• period .
• dash -

(The prefix name must start with a letter.)

Write a solution to find the users who have valid emails.
Return the result table in any order.

Explaination

Question

Table name: Products

Column Name	Type
product_id	int
product_name	varchar
product_category	varchar

This table contains data about the company’s products.

Table name: Orders

Column Name	Type
product_id	int
order_date	date
unit	int

unit is the number of products ordered in order_date.

Write a solution to get the names of products,
that have at least 100 units ordered in February 2020 and their amount.
Return the result table in any order.

Explaination

Retrieve the amount of products

Question

Table name: Activities

Column Name	Type
sell_date	date
product	varchar

Each row of this table contains the product name and the date it was sold in a market.

Write a solution to find for each date the number of different products sold and their names.
The sold products names for each date should be sorted lexicographically.
Return the result table ordered by sell_date.

Explaination

Again, there are two tasks we need to solve:

1. Count how many types of products are sold in one day
2. List all types of items into a single column

Type of Items

We can simply count how many products are sold using COUNT, groupped by the date they belong to:

Question

Table name: ``

Column Name	Type
id	int
salary	int

Each row of this table contains information about the salary of an employee.

Write a solution to find the second highest distinct salary from the Employee table.
If there is no second highest salary, return null.

Explaination

The key idea of this question is to get the second value. Here I have two ideas that come to my mind immediately

1. First, order the list according to salary, then fetch the second row.
2. First, find the highest salary, then do another SELECT query based on the highest salary.

1. Using LIMIT and OFFSET

Using LIMIT and OFFSET, we can simply retrieve the second row of a database:

Question

Table name: Person

Column Name	Type
id	int
email	varchar

Each row of this table contains an email. The emails will not contain uppercase letters.

Write a solution to delete all duplicate emails, keeping only one unique email with the smallest id.
For SQL users, please note that you are supposed to write a DELETE statement and not a SELECT one.
The final order of the table does not matter.

Explaination

Usually, people will simply replace the old table with the new table using SELECT to remove the duplicates.
The tricky part of this question is that you cannot create a new table, as the system only checks the original table Person.

Since we cannot use SELECT, the only way to filter out unwanted rows is to use WHERE or HAVING.

First of all, we can call the same table twice by giving them different name temporarily, so that we can compare between rows,

We need to keep the same email which has smaller id, so p.Id > q_Id, then we also need to nake sure that there are acutally duplicate email, so p.Email=q.Email

Question

Table name: Patients

Column Name	Type
patient_id	int
patient_name	varchar
conditions	varchar

conditions contains zero or more code separated by spaces.
This table contains information of the patients in the hospital.

Write a solution to find the patient_id, patient_name, and conditions of the patients who have Type I Diabetes.
Type I Diabetes always starts with DIAB1 prefix. Return the result table in any order.

Explaination

SQL LIKE Operator

In SQL, to extract data that contain certain specified pattern, we can use LIKE in the WHERE clause.
For example, we can use

SELECT * FROM Patients WHERE conditions LIKE 'DIAB1%'

In here, % is a wildcard, refers to any number of characters can exist after the string DIAB1.
DIAB1, DIAB1234, DIAB1eg are valid outputs.