Skip to content

Latest commit

 

History

History
213 lines (147 loc) · 6.23 KB

API-Reference.md

File metadata and controls

213 lines (147 loc) · 6.23 KB
Raw

MPL.js: API Reference

MPL is a library for parsing and evaluating well-formed formulas (wffs) of modal propositional logic.

MPL has a single dependency, formula-parser.

Parsing and displaying wffs

MPL wffs can be represented in four ways:

  • ASCII, for typing
  • JSON, for processing
  • LaTeX, for displaying nicely
  • Unicode, for displaying accessibly

All four are stored in a Wff object, created by providing either the ASCII or JSON representation as input.

In each case:

  • Parentheses and whitespace don't matter.
  • Binary connectives are strictly binary.
  • Propositional variables may be any alphanumeric string.

In the table below, p is a propositional variable, while A and B are arbitrary subwffs.

ASCIIJSONLaTeXUnicode
Propositionp{prop: 'p'}pp
Negation~A{neg: A}\lnot{}A\u00acA
Necessity[]A{nec: A}\Box{}A\u25a1A
Possibility<>A{poss: A}\Diamond{}A\u25caA
Conjunction(A & B){conj: [A, B]}(A\land{}B)(A \u2227 B)
Disjunction(A | B){disj: [A, B]}(A\lor{}B)(A \u2228 B)
Implication(A -> B){impl: [A, B]}(A\rightarrow{}B)(A \u2192 B)
Equivalence(A <-> B){equi: [A, B]}(A\leftrightarrow{}B)(A \u2194 B)

MPL.Wff( asciiOrJSON )

Constructor for MPL wff. Takes either ASCII or JSON representation as input.

// the following are equivalent:
var wff = new MPL.Wff('(p -> []p)');
var wff = new MPL.Wff({impl: [{prop: 'p'}, {nec: {prop: 'p'}}]});

wff.ascii()

Returns the ASCII representation of an MPL wff.

wff.ascii();
// => '(p -> []p)'

wff.json()

Returns the JSON representation of an MPL wff.

wff.json();
// => {impl: [{prop: 'p'}, {nec: {prop: 'p'}}]}

wff.latex()

Returns the LaTeX representation of an MPL wff.

wff.latex();
// => '(p\\rightarrow{}\\Box{}p)'

wff.unicode()

Returns the Unicode representation of an MPL wff.

wff.unicode();
// => '(p \u2192 \u25a1p)'

Kripke models

Mathematically, a Kripke model consists of:

  • a set of states (or worlds)
  • an accessibility relation (i.e., a set of transitions)
  • a valuation (a complete assignment of truth values to each variable at each state)

Specifically, in an MPL Model:

  • Each state has a zero-based index and an assignment.
  • An assignment is an object in which the keys are propositional variable names and the values are booleans.
  • Only true propositional variables are actually stored! All others are automatically interpreted as false.

Models can also be exported to, and imported from, a compact 'model string' notation.

MPL.Model()

Constructor for Kripke model. Takes no initial input.

var model = new MPL.Model();

model.addTransition( source, target )

Adds a transition to the model, given source and target state indices.

// example: a model where states 0 and 1 have been added and not removed
model.addTransition(0, 1);

model.removeTransition( source, target )

Removes a transition from the model, given source and target state indices.

// example: a model where states 0 and 1 have been added and not removed
model.removeTransition(0, 1);

model.getSuccessorsOf( source )

Returns an array of successor states for a given state index.

// example: a model with transitions (0,0) and (0,1)
model.getSuccessorsOf(0);
// => [0, 1]

model.addState( assignment )

Adds a state with a given assignment to the model.

model.addState({'p': true});

model.editState( state, assignment )

Edits the assignment of a state in the model, given a state index and a new partial assignment.

model.editState(0, {'p': false, 'q': true});

model.removeState( state )

Removes a state and all related transitions from the model, given a state index.

model.removeState(0);

model.getStates()

Returns an array containing the assignment (or null) of each state in the model.
(Only true propositional variables are returned in each assignment.)

// example: a model with states 0 and 2 (where state 1 has been removed); 'q' is true at 0, nothing true at 2
model.getStates();
// => [{'q': true}, null, {}]

model.valuation( propvar, state )

Returns the truth value of a given propositional variable at a given state index.

// example: a model where only 'q' is true at state 0
model.valuation('r', 0);
// => false

model.getModelString()

Returns current model as a compact string suitable for use as a URL parameter.

// example: a model with states 0 and 2 (where state 1 has been removed) and transitions (0,0) and (0,2);
//          'q' is true at 0, nothing true at 2
model.getModelString();
// => 'AqS0,2;;AS;'

model.loadFromModelString( modelString )

Restores a model from a given model string.

model.loadFromModelString('AqS0,2;;AS;');

Evaluating wffs

MPL.truth( model, state, wff )

Evaluate the truth of an MPL wff at a given state within a given model.

// example: model is an MPL Model with only state 0 and no transitions; 'p' is true at state 0
//          wff is the MPL Wff '(p -> []p)'  
MPL.truth(model, 0, wff);
// => true