Skip to content
Snippets Groups Projects
Commit 46426271 authored by Jaime Arias's avatar Jaime Arias
Browse files

Merge branch 'feature/cosyverif' into develop

parents c5d292fb 345f720b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
cosyverif/adtree.fml 0 → 100644
+ 136
− 0
View file @ 46426271
<?xml version="1.0" encoding="UTF-8"?>
<!-- ================================================ -->
<!-- Attack-Defence Tree definition -->
<!-- -->
<!-- Notes : -->
<!-- 1) functions ? -->
<!-- 2) conditions ? -->
<!-- 3) attributes, fixed or dynamic ? -->
<!-- 3) agents ? -->
<!-- ================================================ -->
<formalism name="ADTree" xmlns="http://cosyverif.org/ns/formalism"
xmlns:grml="http://cosyverif.org/ns/model"
xmlns:sch="http://purl.oclc.org/dsdl/schematron">
<!-- ADTree global attributes -->
<leafAttribute name="root" refType="ADTree"/>
<!-- ADTree objects -->
<arcType name="arc"/>
<nodeType name="leaf"/>
<nodeType name="AND"/>
<nodeType name="SAND"/>
<nodeType name="CAND"/>
<nodeType name="SCAND"/>
<nodeType name="OR"/>
<nodeType name="SOR"/>
<nodeType name="COR"/>
<nodeType name="SCOR"/>
<!-- leaf object attributes -->
<leafAttribute name="name" refType="leaf" defaultValue=""/>
<leafAttribute name="role" refType="leaf" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="leaf" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- AND object attributes -->
<leafAttribute name="name" refType="AND" defaultValue=""/>
<leafAttribute name="role" refType="AND" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="AND" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- SAND object attributes -->
<leafAttribute name="name" refType="SAND" defaultValue=""/>
<leafAttribute name="role" refType="SAND" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="SAND" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- CAND object attributes -->
<leafAttribute name="name" refType="CAND" defaultValue=""/>
<leafAttribute name="role" refType="CAND" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="CAND" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- SCAND object attributes -->
<leafAttribute name="name" refType="SCAND" defaultValue=""/>
<leafAttribute name="role" refType="SCAND" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="SCAND" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- OR object attributes -->
<leafAttribute name="name" refType="OR" defaultValue=""/>
<leafAttribute name="role" refType="OR" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="OR" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- SOR object attributes -->
<leafAttribute name="name" refType="SOR" defaultValue=""/>
<leafAttribute name="role" refType="SOR" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="SOR" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- COR object attributes -->
<leafAttribute name="name" refType="COR" defaultValue=""/>
<leafAttribute name="role" refType="COR" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="COR" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- SCOR object attributes -->
<leafAttribute name="name" refType="SCOR" defaultValue=""/>
<leafAttribute name="role" refType="SCOR" defaultValue="ATTACK"/>
<complexAttribute name="attributes" refType="SCOR" >
<child refName="attribute" minOccurs="0" />
</complexAttribute>
<!-- gates attributes -->
<complexAttribute name="attribute">
<child refName="name" minOccurs="1" maxOccurs="1" />
<child refName="value" minOccurs="1" maxOccurs="1" />
</complexAttribute>
<leafAttribute name="name" defaultValue=""/>
<leafAttribute name="value" defaultValue="0"/>
<!-- rule definitions -->
<sch:let name="leaves" value="//grml:node[@nodeType = 'leaf']"/>
<sch:let name="gates" value="//grml:node[@nodeType != 'leaf']"/>
<sch:let name="countergates" value="('CAND', 'SCAND', 'COR', 'SCOR')"/>
<!-- role is a value in {ATTACK, DEFENCE} -->
<sch:rule context="grml:node/grml:attribute[@name = 'role']">
<sch:assert test=". = 'ATTACK' or . = 'DEFENCE'">Role must be either Attack or Defence</sch:assert>
</sch:rule>
<!-- root must not be empty -->
<sch:rule context="grml:attribute[@name='root']">
<sch:assert test="data(.)">Root is not defined</sch:assert>
</sch:rule>
<!-- leaves has no children -->
<sch:rule context="grml:arc">
<sch:assert test="empty(index-of($leaves/@id, @source))">Leaf with id=<sch:value-of select="@source"/> must not have a child</sch:assert>
</sch:rule>
<!-- countering nodes only must have one child with inversed role -->
<sch:rule context="grml:node[@nodeType=$countergates]">
<sch:let name="gate_id" value="@id"/>
<sch:let name="gate_role" value="grml:attribute[@name='role']"/>
<sch:let name="children" value="//grml:arc[@source=$gate_id]/@target"/>
<sch:let name="counter_children" value="//grml:node[@id=$children and grml:attribute[@name='role'] != $gate_role]/@id"/>
<sch:assert test="count($counter_children) = 1">Counter gate with id=<sch:value-of select="$gate_id"/> must have one child with inverse role</sch:assert>
</sch:rule>
</formalism>
cosyverif/treasure_hunters.grml 0 → 100644
+ 176
− 0
View file @ 46426271
<?xml version="1.0" encoding="UTF-8"?>
<model formalismUrl="adtree.fml"
xmlns="http://cosyverif.org/ns/model">
<!-- root gate -->
<attribute name="root">9</attribute>
<!-- ================================================ -->
<!-- Leaves -->
<!-- ================================================ -->
<!-- bribe gatekeeper (leaf b) -->
<node id="1" nodeType="leaf">
<attribute name="name">bribe gatekeeper</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">500</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">60</attribute>
</attribute>
</attribute>
</node>
<!-- force arm. door (leaf f) -->
<node id="2" nodeType="leaf">
<attribute name="name">force arm. door</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">100</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">120</attribute>
</attribute>
</attribute>
</node>
<!-- helicopter (leaf h) -->
<node id="3" nodeType="leaf">
<attribute name="name">helicopter</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">500</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">3</attribute>
</attribute>
</attribute>
</node>
<!-- emergency exit (leaf e) -->
<node id="4" nodeType="leaf">
<attribute name="name">emergency exit</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">0</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">10</attribute>
</attribute>
</attribute>
</node>
<!-- police (leaf p) -->
<node id="5" nodeType="leaf">
<attribute name="name">police</attribute>
<attribute name="role">DEFENCE</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">100</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">10</attribute>
</attribute>
</attribute>
</node>
<!-- ================================================ -->
<!-- Gates -->
<!-- ================================================ -->
<!-- steal treasure (ST) -->
<node id="6" nodeType="AND">
<attribute name="name">steal treasure</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">0</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">2</attribute>
</attribute>
</attribute>
</node>
<!-- get away (GA) -->
<node id="7" nodeType="OR">
<attribute name="name">get away</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">0</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">0</attribute>
</attribute>
</attribute>
</node>
<!-- thieves fleeing (TF) -->
<node id="8" nodeType="SAND">
<attribute name="name">thieves fleeing</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">0</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">0</attribute>
</attribute>
</attribute>
</node>
<!-- treasure stolen (TS) -->
<node id="9" nodeType="CAND">
<attribute name="name">treasure stolen</attribute>
<attribute name="role">ATTACK</attribute>
<attribute name="attributes">
<attribute name="attribute">
<attribute name="name">cost</attribute>
<attribute name="value">0</attribute>
</attribute>
<attribute name="attribute">
<attribute name="name">time</attribute>
<attribute name="value">0</attribute>
</attribute>
</attribute>
</node>
<!-- ================================================ -->
<!-- Arcs -->
<!-- ================================================ -->
<arc id="10" arcType="arc" source="6" target="1"/> <!-- ST->b -->
<arc id="11" arcType="arc" source="6" target="2"/> <!-- ST->f -->
<arc id="12" arcType="arc" source="7" target="3"/> <!-- GA->h -->
<arc id="13" arcType="arc" source="7" target="4"/> <!-- GA->e -->
<arc id="14" arcType="arc" source="8" target="6"/> <!-- TF->ST -->
<arc id="15" arcType="arc" source="8" target="7"/> <!-- TF->GA -->
<arc id="16" arcType="arc" source="9" target="8"/> <!-- TS->TF -->
<arc id="17" arcType="arc" source="9" target="5"/> <!-- TS->p -->
</model>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment