Tutorial

This is an (in progress) tutorial for the library. It will hopefully include small examples that have been tested in Go's playground and can easily be replicated.

Transition Systems

We will assume a (finite) Transition System is described as is done in Definition 2.1 of Baier and Katoen. In fact, in the code the TransitionSystem object has the same components

type TransitionSystem struct {
	S          []TransitionSystemState
	Act        []string
	Transition map[TransitionSystemState]map[string][]TransitionSystemState
	I          []TransitionSystemState // Set of Initial States
	AP         []AtomicProposition
	L          map[TransitionSystemState][]AtomicProposition
}

Rather than worry about creating one of these from scratch there are several built-in functions which can be used to get one that you can play with.

We can easily construct the Beverage Vending Machine Transition System using the built-in function GetBeverageVendingMachineTS():

package main

import (
	"fmt"
	mc "github.com/kwesiRutledge/ModelChecking"
)

func main() {	
	vm := mc.GetBeverageVendingMachineTS()
	
	payState := vm.S[0]
	fmt.Println(payState.Name)
}

As is shown in the example program, you can extract states by indexing from the slice S in the transition system state space (e.g. stateI := vm.S[i]) and each state has a name.

In

For an arbitrary state, we can identify if it's in the initial state set using the method In(). (You can also use In() with other slices of TransitionSystemState() objects.)

package main

import (
	"fmt"
	mc "github.com/kwesiRutledge/ModelChecking"
)

func main() {
	
	vm := mc.GetBeverageVendingMachineTS()
	
	payState := vm.S[0]
	fmt.Println(payState.Name)
	
	tf := payState.In(vm.I)
	fmt.Println(tf)
}

In is used in the definition of the satisfaction operator Satisfies() (among other things).

Satisfies

Identifying if an atomic proposition is satisfied is as simple as creating an atomic proposition object (for example ap1 := AtomicProposition{Name: "paid"}) and then using the method Satisfies() on it for some given state.

package main

import (
	"fmt"
	mc "github.com/kwesiRutledge/ModelChecking"
)

func main() {
	
	vm := mc.GetBeverageVendingMachineTS()
	
	payState := vm.S[1]
	fmt.Println(payState.Name)
	
	apI := mc.AtomicProposition{Name: "paid"}
	
	satisfiesFlag, err := payState.Satisfies(apI)
	if err != nil {
		fmt.Println(fmt.Sprintf("There was an issue running Satisfies: %v",err))
	}
	fmt.Println(satisfiesFlag)
	
}