learning_tla/bin/tlceval.go
2025-02-20 16:06:09 +01:00

71 lines
1.8 KiB
Go

// This program parses the output of TLC in -tool mode on stdin,
// considering only the first line matching the output of an ASSUME PrintT("Eval", foo)),
// and outputs the value of foo on stdout.
package main
import (
"bufio"
"bytes"
"fmt"
"log"
"os"
"regexp"
"strconv"
"strings"
)
type Message struct {
MsgID int `json:"msg_id"`
Content string `json:"content"`
}
var (
startMsgRegex = regexp.MustCompile(`@!@!@STARTMSG (\d+):\d+ @!@!@`)
endMsgRegex = regexp.MustCompile(`@!@!@ENDMSG \d+ @!@!@`)
evalRegex = regexp.MustCompile(`(?m)<<\s*"Eval",(.*)>>`)
)
func main() {
scanner := bufio.NewScanner(os.Stdin)
var messages []Message
var currentMessage Message
var contentBuffer bytes.Buffer
for scanner.Scan() {
messages = scan(scanner, &currentMessage, &contentBuffer, messages)
}
if err := scanner.Err(); err != nil {
log.Fatalf("error reading file: %s", err)
}
for _, message := range messages {
if s := evalRegex.FindStringSubmatch(message.Content); len(s) == 2 {
fmt.Println(strings.TrimSpace(s[1]))
}
}
}
func scan(scanner *bufio.Scanner, currentMessage *Message, contentBuffer *bytes.Buffer, messages []Message) []Message {
line := scanner.Text()
if matches := startMsgRegex.FindStringSubmatch(line); matches != nil {
if currentMessage.MsgID != 0 {
currentMessage.Content = contentBuffer.String()
messages = append(messages, *currentMessage)
contentBuffer.Reset()
}
n, err := strconv.Atoi(matches[1])
if err != nil {
log.Fatalf("error converting string to int: %s", err)
}
currentMessage.MsgID = n
} else if endMsgRegex.MatchString(line) {
currentMessage.Content = contentBuffer.String()
messages = append(messages, *currentMessage)
contentBuffer.Reset()
*currentMessage = Message{}
} else {
contentBuffer.WriteString(strings.TrimSpace(line) + " ")
}
return messages
}