2021.07.26

Date	2021-07-26
Person	@KevinTung

Context and Goal

Resolved conflict with Ben and align with Jared.

To-Do

• Prepare meeting with Ben
• Install TLA,and K-framework

Progress

• I had researched for TLA deployment for about one hour. The question I had is that TLA+ was a desktop-based application with graphic user interface (based on the information on the official page). If we want to deploy it on the web, we should turn it into a web application. Then I was searching how it is possible to do this. There were few tools that could convert it and I checked the code base of TLA just to see little documentation. The docker container you offered me was out of my previous consideration. I will take a look at how it turns the tool into a web app, or they just simply developed another version which was not documented on the official website.
  • https://lamport.azurewebsites.net/tla/toolbox.html?back-link=tools.html
• Template:Logic Model 2 needs only one param to generate the required pages. Also when you click the parameter type (like Goal), you will be directed to the related pages
  • https://thewiki.us/index.php/Job/K8s_Installation
• Ben: https://github.com/talex5/tla; https://github.com/kframework/kore
• Ben: Should have done researched and double-checked
• Finished the bi-weekly report to Tsinghua.