1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

// alloy-viz renders Alloy instances in a browser, without the Alloy GUI.
//
// Point it at a .als file; it solves the selected command and shows the instance
// as a graph, re-solving whenever you save. Keep editing in your own editor --
// the browser is a viewer.
//
// One model per process: to watch a second file, run a second alloy-viz on
// another port.
package main

import (
	"errors"
	"flag"
	"fmt"
	"log"
	"net"
	"net/http"
	"os"
	"os/signal"
	"path/filepath"
	"strings"
	"syscall"
	"time"
)

func main() {
	log.SetFlags(log.Ltime)

	var (
		addr       = flag.String("addr", "127.0.0.1:8791", "address for the web UI")
		noOpen     = flag.Bool("no-run", false, "do not solve on startup; wait for a command to be chosen")
		commandIdx = flag.Int("command", 0, "index of the command to run initially")
	)
	flag.Usage = usage
	flag.Parse()

	if flag.NArg() != 1 {
		usage()
		os.Exit(2)
	}
	path, err := filepath.Abs(flag.Arg(0))
	if err != nil {
		fatal(err)
	}
	if _, err := os.Stat(path); err != nil {
		fatal(err)
	}
	if !strings.HasSuffix(path, ".als") {
		log.Printf("warning: %s does not look like an Alloy model", path)
	}
	srv := newServer(path)
	srv.selected = *commandIdx
	defer srv.Shutdown()

	// Ctrl-C must kill the JVM too, or it lingers holding a SAT solver.
	sigs := make(chan os.Signal, 1)
	signal.Notify(sigs, os.Interrupt, syscall.SIGTERM)
	go func() {
		<-sigs
		log.Print("shutting down")
		srv.Shutdown()
		os.Exit(0)
	}()

	// Watch before the first solve, so an edit during a slow startup is not lost.
	go func() {
		if err := watchFile(srv.path, func() {
			log.Printf("%s changed, re-running", filepath.Base(srv.path))
			srv.Invalidate()
			srv.Reload(true)
		}); err != nil {
			log.Printf("watch: %v", err)
		}
	}()

	go srv.Reload(!*noOpen)

	ln, err := net.Listen("tcp", *addr)
	if err != nil {
		fatal(err)
	}

	log.Printf("alloy-viz on http://%s  (%s)", ln.Addr(), srv.path)

	httpSrv := &http.Server{
		Handler: srv.Handler(),
		// No write timeout: SSE streams stay open for the length of a solve,
		// which can exceed any sensible bound.
		ReadHeaderTimeout: 10 * time.Second,
	}
	if err := httpSrv.Serve(ln); err != nil && !errors.Is(err, http.ErrServerClosed) {
		fatal(err)
	}
}

func usage() {
	fmt.Fprintf(os.Stderr, `alloy-viz — view Alloy instances in a browser

usage: alloy-viz [flags] <model.als>

Solves a command from the model and renders the instance as a graph, re-solving
on every save. A sibling <model>.thm theme file is applied if present.

flags:
`)
	flag.PrintDefaults()
	fmt.Fprintf(os.Stderr, `
environment:
  %s  path to the alloy-viz-solver binary (the nix wrapper sets this)

examples:
  alloy-viz model.als
  alloy-viz -command 3 filesystem.als
  alloy-viz -no-run model.als   # pick the command in the browser first
`, solverPathEnv)
}

func fatal(err error) {
	fmt.Fprintf(os.Stderr, "alloy-viz: %v\n", err)
	os.Exit(1)
}